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