Bob is rough. Bob is round. Charlie is blue. Charlie is not furry. Charlie is red. Charlie is rough. Charlie is round. If Bob is red then Bob is cold. If Charlie is cold and Charlie is blue then Charlie is quiet. Round, rough people are cold.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If Bob is red then Bob is cold.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "cold" "+"))
If Charlie is cold and Charlie is blue then Charlie is quiet.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "quiet" "+"))
Round, rough people are cold.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Charlie is not furry.
True
1
proof
[(triple4)]
("Charlie" "is" "furry" "-")
triple4
Charlie is not blue.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "blue" "-")
triple3
Bob is cold.
True
3
proof
[(((triple2 triple1) -> rule3))]
("Bob" "is" "cold" "+")
((triple2 triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is not cold.
False
3
inv-proof
[(((triple7 triple6) -> rule3))]
("Charlie" "is" "cold" "-")
((triple7 triple6) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
True
5
proof
[(((((triple7 triple6) -> rule3) triple3) -> rule2))]
("Charlie" "is" "quiet" "+")
((((triple7 triple6) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not quiet.
False
5
inv-proof
[(((((triple7 triple6) -> rule3) triple3) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple7 triple6) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is rough.[(triple1)] Bob is round.[(triple2)] Charlie is blue.[(triple3)] Charlie is not furry.[(triple4)] Charlie is red.[(triple5)] Charlie is rough.[(triple6)] Charlie is round.[(triple7)] @1: Bob is cold.[(((triple2 triple1) -> rule3))] Charlie is cold.[(((triple7 triple6) -> rule3))] @2: Charlie is quiet.[(((((triple7 triple6) -> rule3) triple3) -> rule2))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple2 triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple7 triple6) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple7 triple6) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2