Erin is cold. Erin is red. Erin is rough. Erin is round. Gary is quiet. Gary is not white. Harry is round. If Gary is cold and Gary is quiet then Gary is big. All round, white things are big. Red, cold things are not big. If Harry is round then Harry is white. If Gary is not round then Gary is not rough. If something is round and quiet then it is cold.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not white.
("Gary" "is" "white" "-")
Harry is round.
("Harry" "is" "round" "+")
If Gary is cold and Gary is quiet then Gary is big.
((("Gary" "is" "cold" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "big" "+"))
All round, white things are big.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Red, cold things are not big.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "big" "-"))
If Harry is round then Harry is white.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "white" "+"))
If Gary is not round then Gary is not rough.
((("Gary" "is" "round" "~")) -> ("Gary" "is" "rough" "-"))
If something is round and quiet then it is cold.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Erin is round.
True
1
proof
[(triple4)]
("Erin" "is" "round" "+")
triple4
Erin is not red.
False
1
inv-proof
[(triple2)]
("Erin" "is" "red" "-")
triple2
Harry is white.
True
2
proof
[(((triple7) -> rule4))]
("Harry" "is" "white" "+")
((triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple7) -> rule4))]
("Harry" "is" "white" "-")
((triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
True
4
proof
[(((triple7 ((triple7) -> rule4)) -> rule2))]
("Harry" "is" "big" "+")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not big.
False
4
inv-proof
[(((triple7 ((triple7) -> rule4)) -> rule2))]
("Harry" "is" "big" "-")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "cold" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "+")
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Gary" "is" "big" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Erin is cold.[(triple1)] Erin is red.[(triple2)] Erin is rough.[(triple3)] Erin is round.[(triple4)] Gary is not white.[(triple6)] Gary is quiet.[(triple5)] Harry is round.[(triple7)] @1: Erin is not big.[(((triple2 triple1) -> rule3))] Harry is white.[(((triple7) -> rule4))] @2: Harry is big.[(((triple7 ((triple7) -> rule4)) -> rule2))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Gary is not white.
("Gary" "is" "white" "-")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple7
Erin is not big.
("Erin" "is" "big" "-")
((triple2 triple1) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7 ((triple7) -> (rule4 % int2))) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2