Bob is blue. Bob is cold. Bob is furry. Bob is kind. Bob is quiet. Bob is round. Bob is smart. Charlie is blue. Charlie is quiet. Charlie is round. Dave is blue. Dave is cold. If someone is smart then they are furry. All quiet, kind people are furry. All furry, blue people are cold. All quiet, blue people are smart. Blue people are cold. If someone is round then they are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All quiet, kind people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All furry, blue people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All quiet, blue people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Bob is kind.
True
1
proof
[(triple4)]
("Bob" "is" "kind" "+")
triple4
Bob is not furry.
False
1
inv-proof
[(triple3 OR ((triple7) -> rule1) OR ((triple5 triple4) -> rule2) OR ((((triple5 triple1) -> rule4)) -> rule1) OR ((((triple5 ((triple6) -> rule6)) -> rule4)) -> rule1))]
("Bob" "is" "furry" "-")
triple3
((triple7) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple5 triple4) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple5 triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5 ((triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Bob is blue.[(triple1 OR ((triple6) -> rule6))] Bob is cold.[(triple2 OR ((triple1) -> rule5) OR ((triple3 triple1) -> rule3) OR ((((triple6) -> rule6)) -> rule5) OR ((triple3 ((triple6) -> rule6)) -> rule3) OR ((((triple7) -> rule1) triple1) -> rule3) OR ((((triple5 triple4) -> rule2) triple1) -> rule3) OR ((((triple7) -> rule1) ((triple6) -> rule6)) -> rule3) OR ((((triple5 triple4) -> rule2) ((triple6) -> rule6)) -> rule3) OR ((((((triple5 triple1) -> rule4)) -> rule1) triple1) -> rule3) OR ((((((triple5 triple1) -> rule4)) -> rule1) ((triple6) -> rule6)) -> rule3) OR ((((((triple5 ((triple6) -> rule6)) -> rule4)) -> rule1) triple1) -> rule3) OR ((((((triple5 ((triple6) -> rule6)) -> rule4)) -> rule1) ((triple6) -> rule6)) -> rule3))] Bob is furry.[(triple3 OR ((triple7) -> rule1) OR ((triple5 triple4) -> rule2) OR ((((triple5 triple1) -> rule4)) -> rule1) OR ((((triple5 ((triple6) -> rule6)) -> rule4)) -> rule1))] Bob is kind.[(triple4)] Bob is quiet.[(triple5)] Bob is round.[(triple6)] Bob is smart.[(triple7 OR ((triple5 triple1) -> rule4) OR ((triple5 ((triple6) -> rule6)) -> rule4))] Charlie is blue.[(triple8 OR ((triple10) -> rule6))] Charlie is quiet.[(triple9)] Charlie is round.[(triple10)] Dave is blue.[(triple11)] Dave is cold.[(triple12 OR ((triple11) -> rule5))] @1: Charlie is cold.[(((triple8) -> rule5) OR ((((triple10) -> rule6)) -> rule5) OR ((((((triple9 triple8) -> rule4)) -> rule1) triple8) -> rule3) OR ((((((triple9 triple8) -> rule4)) -> rule1) ((triple10) -> rule6)) -> rule3) OR ((((((triple9 ((triple10) -> rule6)) -> rule4)) -> rule1) triple8) -> rule3) OR ((((((triple9 ((triple10) -> rule6)) -> rule4)) -> rule1) ((triple10) -> rule6)) -> rule3))] Charlie is smart.[(((triple9 triple8) -> rule4) OR ((triple9 ((triple10) -> rule6)) -> rule4))] @2: Charlie is furry.[(((((triple9 triple8) -> rule4)) -> rule1) OR ((((triple9 ((triple10) -> rule6)) -> rule4)) -> rule1))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple6) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple1) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple3 triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple3 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple7) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple5 triple4) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple7) -> (rule1 % int3)) ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((triple5 triple4) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple5 triple1) -> (rule4 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple5 triple1) -> (rule4 % int4))) -> (rule1 % int3)) ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple5 ((triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
((((((triple5 ((triple6) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((triple6) -> (rule6 % int4))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
triple3
((triple7) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple5 triple4) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple5 triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple5 ((triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((triple5 triple1) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple5 ((triple6) -> (rule6 % int2))) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
((triple10) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
Charlie is round.
("Charlie" "is" "round" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
triple11
Dave is cold.
("Dave" "is" "cold" "+")
triple12
((triple11) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple8) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple9 triple8) -> (rule4 % int3))) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple9 triple8) -> (rule4 % int4))) -> (rule1 % int3)) ((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((triple9 ((triple10) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) triple8) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
((((((triple9 ((triple10) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2)) ((triple10) -> (rule6 % int4))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple9 triple8) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple9 ((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple9 triple8) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((triple9 ((triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3