Bob is kind. Bob is white. Harry is big. Harry is kind. Harry is quiet. Harry is smart. Harry is young. If something is kind then it is young. All smart things are white. White, big things are smart. If something is young and smart then it is quiet. If something is white then it is big. If Harry is kind and Harry is not young then Harry is big.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is kind then it is young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
White, big things are smart.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is young and smart then it is quiet.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is white then it is big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If Harry is kind and Harry is not young then Harry is big.
((("Harry" "is" "kind" "+") ("Harry" "is" "young" "~")) -> ("Harry" "is" "big" "+"))
Harry is quiet.
True
1
proof
[(triple5 OR ((triple7 triple6) -> rule4) OR ((((triple4) -> rule1) triple6) -> rule4))]
("Harry" "is" "quiet" "+")
triple5
((triple7 triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple4) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Bob is big.
True
2
proof
[(((triple2) -> rule5))]
("Bob" "is" "big" "+")
((triple2) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple6) -> rule2))]
("Harry" "is" "white" "-")
((triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is smart.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule3))]
("Bob" "is" "smart" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule3))]
("Bob" "is" "smart" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is kind.[(triple1)] Bob is white.[(triple2)] Harry is big.[(triple3 OR ((((triple6) -> rule2)) -> rule5))] Harry is kind.[(triple4)] Harry is quiet.[(triple5 OR ((triple7 triple6) -> rule4) OR ((((triple4) -> rule1) triple6) -> rule4))] Harry is smart.[(triple6)] Harry is young.[(triple7 OR ((triple4) -> rule1))] @1: Bob is big.[(((triple2) -> rule5))] Bob is young.[(((triple1) -> rule1))] Harry is white.[(((triple6) -> rule2))] @2: Bob is smart.[(((triple2 ((triple2) -> rule5)) -> rule3))] @3: Bob is quiet.[(((((triple1) -> rule1) ((triple2 ((triple2) -> rule5)) -> rule3)) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
((triple7 triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple4) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
((triple4) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int4)) ((triple2 ((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4