Bob is blue. Bob is nice. Bob is white. Charlie is nice. Charlie is round. Charlie is smart. Charlie is white. Charlie is young. Harry is nice. Harry is white. White people are round. If someone is young then they are white. Smart people are white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
Harry is nice.
True
1
proof
[(triple9)]
("Harry" "is" "nice" "+")
triple9
Charlie is not smart.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "smart" "-")
triple6
Harry is round.
True
2
proof
[(((triple10) -> rule1))]
("Harry" "is" "round" "+")
((triple10) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple3) -> rule1))]
("Bob" "is" "round" "-")
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Bob is white.[(triple3)] Charlie is nice.[(triple4)] Charlie is round.[(triple5 OR ((triple7) -> rule1) OR ((((triple6) -> rule3)) -> rule1) OR ((((triple8) -> rule2)) -> rule1))] Charlie is smart.[(triple6)] Charlie is white.[(triple7 OR ((triple6) -> rule3) OR ((triple8) -> rule2))] Charlie is young.[(triple8)] Harry is nice.[(triple9)] Harry is white.[(triple10)] @1: Bob is round.[(((triple3) -> rule1))] Harry is round.[(((triple10) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
((triple7) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple6) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple8) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple10) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1