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