Anne is blue. Anne is rough. Erin is blue. Erin is cold. Gary is round. Harry is red. Harry is rough. Big, rough things are cold. If Gary is blue and Gary is quiet then Gary is red. All red things are cold. Round, big things are blue. If something is round and blue then it is quiet. If something is round then it is big. Red things are cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Big, rough things are cold.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If Gary is blue and Gary is quiet then Gary is red.
((("Gary" "is" "blue" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "red" "+"))
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Round, big things are blue.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is round and blue then it is quiet.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
Erin is blue.
True
1
proof
[(triple3)]
("Erin" "is" "blue" "+")
triple3
Harry is not rough.
False
1
inv-proof
[(triple7)]
("Harry" "is" "rough" "-")
triple7
Harry is cold.
True
2
proof
[(((triple6) -> rule3) OR ((triple6) -> rule7))]
("Harry" "is" "cold" "+")
((triple6) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple6) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple5) -> rule6))]
("Gary" "is" "big" "-")
((triple5) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is blue.
True
4
proof
[(((triple5 ((triple5) -> rule6)) -> rule4))]
("Gary" "is" "blue" "+")
((triple5 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not blue.
False
4
inv-proof
[(((triple5 ((triple5) -> rule6)) -> rule4))]
("Gary" "is" "blue" "-")
((triple5 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
True
6
proof
[(((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5))]
("Gary" "is" "quiet" "+")
((triple5 ((triple5 ((triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not quiet.
False
6
inv-proof
[(((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5))]
("Gary" "is" "quiet" "-")
((triple5 ((triple5 ((triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
True
11
proof
[(((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2))]
("Gary" "is" "red" "+")
((((triple5 ((triple5) -> (rule6 % int4))) -> (rule4 % int3)) ((triple5 ((triple5 ((triple5) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is not red.
False
11
inv-proof
[(((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2))]
("Gary" "is" "red" "-")
((((triple5 ((triple5) -> (rule6 % int4))) -> (rule4 % int3)) ((triple5 ((triple5 ((triple5) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is cold.
True
12
proof
[(((((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2)) -> rule3) OR ((((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2)) -> rule7))]
("Gary" "is" "cold" "+")
((((((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5 ((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
((((((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5 ((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Gary is not cold.
False
12
inv-proof
[(((((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2)) -> rule3) OR ((((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2)) -> rule7))]
("Gary" "is" "cold" "-")
((((((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5 ((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
((((((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5 ((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Anne is not big.
Unknown
inv-rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "quiet" "+")
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "blue" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "big" "+")
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Anne" "is" "cold" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "big" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is blue.[(triple1)] Anne is rough.[(triple2)] Erin is blue.[(triple3)] Erin is cold.[(triple4)] Gary is round.[(triple5)] Harry is red.[(triple6)] Harry is rough.[(triple7)] @1: Gary is big.[(((triple5) -> rule6))] Harry is cold.[(((triple6) -> rule3) OR ((triple6) -> rule7))] @2: Gary is blue.[(((triple5 ((triple5) -> rule6)) -> rule4))] @3: Gary is quiet.[(((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5))] @4: Gary is red.[(((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2))] @5: Gary is cold.[(((((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2)) -> rule3) OR ((((((triple5 ((triple5) -> rule6)) -> rule4) ((triple5 ((triple5 ((triple5) -> rule6)) -> rule4)) -> rule5)) -> rule2)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
((triple5) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple6) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple6) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple5 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple5 ((triple5 ((triple5) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((((triple5 ((triple5) -> (rule6 % int4))) -> (rule4 % int3)) ((triple5 ((triple5 ((triple5) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5 ((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
((((((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4)) ((triple5 ((triple5 ((triple5) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5