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