Charlie is blue. Charlie is nice. Charlie is red. Charlie is round. Charlie is white. Dave is kind. Dave is nice. Dave is quiet. Dave is red. Dave is round. Dave is white. Gary is kind. Gary is nice. Gary is quiet. Gary is red. Gary is round. All red, nice people are white. All blue, kind people are round. All blue, nice people are quiet. Blue people are quiet. If Gary is nice and Gary is kind then Gary is blue. If someone is nice and white then they are red. Nice, red people are quiet. If Gary is white and Gary is quiet then Gary is nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
All red, nice people are white.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
All blue, kind people are round.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All blue, nice people are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is nice and Gary is kind then Gary is blue.
((("Gary" "is" "nice" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "blue" "+"))
If someone is nice and white then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Nice, red people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is white and Gary is quiet then Gary is nice.
((("Gary" "is" "white" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "nice" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Dave is not white.
False
1
inv-proof
[(triple11 OR ((triple9 triple7) -> rule1))]
("Dave" "is" "white" "-")
triple11
((triple9 triple7) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is blue.[(triple1)] Charlie is nice.[(triple2)] Charlie is red.[(triple3 OR ((triple2 triple5) -> rule6))] Charlie is round.[(triple4)] Charlie is white.[(triple5 OR ((triple3 triple2) -> rule1))] Dave is kind.[(triple6)] Dave is nice.[(triple7)] Dave is quiet.[(triple8 OR ((triple7 triple9) -> rule7) OR ((triple7 ((triple7 triple11) -> rule6)) -> rule7))] Dave is red.[(triple9 OR ((triple7 triple11) -> rule6))] Dave is round.[(triple10)] Dave is white.[(triple11 OR ((triple9 triple7) -> rule1))] Gary is kind.[(triple12)] Gary is nice.[(triple13)] Gary is quiet.[(triple14 OR ((triple13 triple15) -> rule7) OR ((((triple13 triple12) -> rule5)) -> rule4) OR ((((triple13 triple12) -> rule5) triple13) -> rule3))] Gary is red.[(triple15)] Gary is round.[(triple16 OR ((((triple13 triple12) -> rule5) triple12) -> rule2))] @1: Charlie is quiet.[(((triple1) -> rule4) OR ((triple1 triple2) -> rule3) OR ((triple2 triple3) -> rule7) OR ((triple2 ((triple2 triple5) -> rule6)) -> rule7))] Gary is blue.[(((triple13 triple12) -> rule5))] Gary is white.[(((triple15 triple13) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
((triple2 triple5) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
((triple3 triple2) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple7 triple9) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple7 ((triple7 triple11) -> (rule6 % int2))) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple7 triple11) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
((triple9 triple7) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple12
Gary is nice.
("Gary" "is" "nice" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
((triple13 triple15) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple13 triple12) -> (rule5 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple13 triple12) -> (rule5 % int2)) triple13) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple15
Gary is round.
("Gary" "is" "round" "+")
triple16
((((triple13 triple12) -> (rule5 % int2)) triple12) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1 triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2 triple3) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2 ((triple2 triple5) -> (rule6 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple13 triple12) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple15 triple13) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1