Bob is cold. Bob is green. Bob is red. Bob is white. Charlie is cold. Charlie is green. Charlie is quiet. Charlie is round. Charlie is white. Dave is big. Dave is cold. Dave is green. Dave is quiet. Dave is red. Dave is white. All big, red things are green. If Dave is red then Dave is white. Red, green things are round.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
All big, red things are green.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Dave is red then Dave is white.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "white" "+"))
Red, green things are round.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Bob is white.
True
1
proof
[(triple4)]
("Bob" "is" "white" "+")
triple4
Dave is not cold.
False
1
inv-proof
[(triple11)]
("Dave" "is" "cold" "-")
triple11
Dave is round.
True
3
proof
[(((triple14 triple12) -> rule3) OR ((triple14 ((triple10 triple14) -> rule1)) -> rule3))]
("Dave" "is" "round" "+")
((triple14 triple12) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple14 ((triple10 triple14) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Bob is not round.
False
3
inv-proof
[(((triple3 triple2) -> rule3))]
("Bob" "is" "round" "-")
((triple3 triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is red.[(triple3)] Bob is white.[(triple4)] Charlie is cold.[(triple5)] Charlie is green.[(triple6)] Charlie is quiet.[(triple7)] Charlie is round.[(triple8)] Charlie is white.[(triple9)] Dave is big.[(triple10)] Dave is cold.[(triple11)] Dave is green.[(triple12 OR ((triple10 triple14) -> rule1))] Dave is quiet.[(triple13)] Dave is red.[(triple14)] Dave is white.[(triple15 OR ((triple14) -> rule2))] @1: Bob is round.[(((triple3 triple2) -> rule3))] Dave is round.[(((triple14 triple12) -> rule3) OR ((triple14 ((triple10 triple14) -> rule1)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Dave is big.
("Dave" "is" "big" "+")
triple10
Dave is cold.
("Dave" "is" "cold" "+")
triple11
Dave is green.
("Dave" "is" "green" "+")
triple12
((triple10 triple14) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple13
Dave is red.
("Dave" "is" "red" "+")
triple14
Dave is white.
("Dave" "is" "white" "+")
triple15
((triple14) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3 triple2) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple14 triple12) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple14 ((triple10 triple14) -> (rule1 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2