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