Bob is big. Bob is blue. Bob is furry. Bob is green. Bob is kind. Bob is quiet. Bob is round. Charlie is big. Charlie is blue. Charlie is furry. Charlie is green. Charlie is quiet. Charlie is round. Gary is blue. Gary is kind. Gary is round. Kind, round people are blue. If someone is kind then they are big. Blue people are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Kind, round people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Bob is big.
True
1
proof
[(triple1 OR ((triple5) -> rule2) OR ((((triple2) -> rule3)) -> rule2))]
("Bob" "is" "big" "+")
triple1
((triple5) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Charlie is not round.
False
1
inv-proof
[(triple13)]
("Charlie" "is" "round" "-")
triple13
Gary is big.
True
2
proof
[(((triple15) -> rule2) OR ((((triple14) -> rule3)) -> rule2))]
("Gary" "is" "big" "+")
((triple15) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not big.
False
2
inv-proof
[(((triple15) -> rule2) OR ((((triple14) -> rule3)) -> rule2))]
("Gary" "is" "big" "-")
((triple15) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Bob is big.[(triple1 OR ((triple5) -> rule2) OR ((((triple2) -> rule3)) -> rule2))] Bob is blue.[(triple2 OR ((triple5 triple7) -> rule1))] Bob is furry.[(triple3)] Bob is green.[(triple4)] Bob is kind.[(triple5 OR ((triple2) -> rule3))] Bob is quiet.[(triple6)] Bob is round.[(triple7)] Charlie is big.[(triple8 OR ((((triple9) -> rule3)) -> rule2))] Charlie is blue.[(triple9)] Charlie is furry.[(triple10)] Charlie is green.[(triple11)] Charlie is quiet.[(triple12)] Charlie is round.[(triple13)] Gary is blue.[(triple14 OR ((triple15 triple16) -> rule1))] Gary is kind.[(triple15 OR ((triple14) -> rule3))] Gary is round.[(triple16)] @1: Charlie is kind.[(((triple9) -> rule3))] Gary is big.[(((triple15) -> rule2) OR ((((triple14) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple5) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple5 triple7) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Bob is round.
("Bob" "is" "round" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
triple8
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple9
Charlie is furry.
("Charlie" "is" "furry" "+")
triple10
Charlie is green.
("Charlie" "is" "green" "+")
triple11
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple12
Charlie is round.
("Charlie" "is" "round" "+")
triple13
Gary is blue.
("Gary" "is" "blue" "+")
triple14
((triple15 triple16) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple15
((triple14) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple16
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple9) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple15) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2