Anne is green. Dave is big. Dave is cold. Dave is nice. Gary is green. Gary is nice. Gary is quiet. Harry is blue. Harry is nice. Harry is quiet. All quiet things are smart. If something is smart and green then it is cold. All quiet, big things are green. Blue, green things are nice. If Anne is blue and Anne is smart then Anne is big. If something is green then it is big. If something is big and nice then it is quiet. Big things are blue.
Anne is green.
("Anne" "is" "green" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is smart and green then it is cold.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
All quiet, big things are green.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Blue, green things are nice.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If Anne is blue and Anne is smart then Anne is big.
((("Anne" "is" "blue" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "big" "+"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is big and nice then it is quiet.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Gary is green.
True
1
proof
[(triple5)]
("Gary" "is" "green" "+")
triple5
Harry is not blue.
False
1
inv-proof
[(triple8)]
("Harry" "is" "blue" "-")
triple8
Anne is big.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "big" "+")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple7) -> rule1) OR ((((((triple5) -> rule6) triple6) -> rule7)) -> rule1) OR ((((((triple5) -> rule6) ((((((triple5) -> rule6)) -> rule8) triple5) -> rule4)) -> rule7)) -> rule1))]
("Gary" "is" "smart" "-")
((triple7) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((((triple5) -> (rule6 % int3)) triple6) -> (rule7 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple5) -> (rule6 % int5)) ((((((triple5) -> (rule6 % int5))) -> (rule8 % int4)) triple5) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Dave is smart.
True
4
proof
[(((((triple2 triple4) -> rule7)) -> rule1))]
("Dave" "is" "smart" "+")
((((triple2 triple4) -> (rule7 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule8))]
("Gary" "is" "blue" "-")
((((triple5) -> (rule6 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Anne is nice.
True
5
proof
[(((((((triple1) -> rule6)) -> rule8) triple1) -> rule4))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not nice.
False
5
inv-proof
[(((((((triple1) -> rule6)) -> rule8) triple1) -> rule4))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is quiet.
True
8
proof
[(((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule8) triple1) -> rule4)) -> rule7))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4))) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not quiet.
False
8
inv-proof
[(((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule8) triple1) -> rule4)) -> rule7))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4))) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is smart.
True
9
proof
[(((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule8) triple1) -> rule4)) -> rule7)) -> rule1))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule6 % int5)) ((((((triple1) -> (rule6 % int5))) -> (rule8 % int4)) triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Anne is not smart.
False
9
inv-proof
[(((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule8) triple1) -> rule4)) -> rule7)) -> rule1))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule6 % int5)) ((((((triple1) -> (rule6 % int5))) -> (rule8 % int4)) triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is cold.
Unknown
rconc
[@3: Harry is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule6 <- FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is green.[(triple1)] Dave is big.[(triple2)] Dave is cold.[(triple3 OR ((((((triple2 triple4) -> rule7)) -> rule1) ((((triple2 triple4) -> rule7) triple2) -> rule3)) -> rule2))] Dave is nice.[(triple4)] Gary is green.[(triple5)] Gary is nice.[(triple6 OR ((((((triple5) -> rule6)) -> rule8) triple5) -> rule4))] Gary is quiet.[(triple7 OR ((((triple5) -> rule6) triple6) -> rule7) OR ((((triple5) -> rule6) ((((((triple5) -> rule6)) -> rule8) triple5) -> rule4)) -> rule7))] Harry is blue.[(triple8)] Harry is nice.[(triple9)] Harry is quiet.[(triple10)] @1: Anne is big.[(((triple1) -> rule6))] Dave is blue.[(((triple2) -> rule8))] Dave is quiet.[(((triple2 triple4) -> rule7))] Gary is big.[(((triple5) -> rule6))] Gary is smart.[(((triple7) -> rule1) OR ((((((triple5) -> rule6) triple6) -> rule7)) -> rule1) OR ((((((triple5) -> rule6) ((((((triple5) -> rule6)) -> rule8) triple5) -> rule4)) -> rule7)) -> rule1))] Harry is smart.[(((triple10) -> rule1))] @2: Anne is blue.[(((((triple1) -> rule6)) -> rule8))] Dave is green.[(((((triple2 triple4) -> rule7) triple2) -> rule3))] Dave is smart.[(((((triple2 triple4) -> rule7)) -> rule1))] Gary is blue.[(((((triple5) -> rule6)) -> rule8))] Gary is cold.[(((((triple7) -> rule1) triple5) -> rule2) OR ((((((((triple5) -> rule6) triple6) -> rule7)) -> rule1) triple5) -> rule2) OR ((((((((triple5) -> rule6) ((((((triple5) -> rule6)) -> rule8) triple5) -> rule4)) -> rule7)) -> rule1) triple5) -> rule2))] @3: Anne is nice.[(((((((triple1) -> rule6)) -> rule8) triple1) -> rule4))] @4: Anne is quiet.[(((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule8) triple1) -> rule4)) -> rule7))] @5: Anne is smart.[(((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule8) triple1) -> rule4)) -> rule7)) -> rule1))] @6: Anne is cold.[(((((((((triple1) -> rule6) ((((((triple1) -> rule6)) -> rule8) triple1) -> rule4)) -> rule7)) -> rule1) triple1) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
((((((triple2 triple4) -> (rule7 % int4))) -> (rule1 % int3)) ((((triple2 triple4) -> (rule7 % int4)) triple2) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
((((((triple5) -> (rule6 % int3))) -> (rule8 % int2)) triple5) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
((((triple5) -> (rule6 % int2)) triple6) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple5) -> (rule6 % int4)) ((((((triple5) -> (rule6 % int4))) -> (rule8 % int3)) triple5) -> (rule4 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple2) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2 triple4) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple5) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((((triple5) -> (rule6 % int3)) triple6) -> (rule7 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple5) -> (rule6 % int5)) ((((((triple5) -> (rule6 % int5))) -> (rule8 % int4)) triple5) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
int5
Harry is smart.
("Harry" "is" "smart" "+")
((triple10) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple2 triple4) -> (rule7 % int2)) triple2) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2 triple4) -> (rule7 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple5) -> (rule6 % int2))) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple7) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((((((triple5) -> (rule6 % int4)) triple6) -> (rule7 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((((((triple5) -> (rule6 % int6)) ((((((triple5) -> (rule6 % int6))) -> (rule8 % int5)) triple5) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
int5
Gary is big.
("Gary" "is" "big" "+")
int6
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4))) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule6 % int5)) ((((((triple1) -> (rule6 % int5))) -> (rule8 % int4)) triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Anne is cold.
("Anne" "is" "cold" "+")
((((((((triple1) -> (rule6 % int6)) ((((((triple1) -> (rule6 % int6))) -> (rule8 % int5)) triple1) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Anne is big.
("Anne" "is" "big" "+")
int6