Anne is big. Bob is furry. Bob is green. Bob is red. Bob is round. Charlie is furry. Charlie is green. Quiet things are kind. If something is quiet then it is furry. If something is big then it is red. All kind, big things are round. Quiet things are big. If something is round then it is furry. All furry, green things are quiet. If something is round then it is red.
Anne is big.
("Anne" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All kind, big things are round.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All furry, green things are quiet.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Bob is round.
True
1
proof
[(triple5 OR ((((((triple2 triple3) -> rule7)) -> rule1) ((((triple2 triple3) -> rule7)) -> rule5)) -> rule4))]
("Bob" "is" "round" "+")
triple5
((((((triple2 triple3) -> (rule7 % int4))) -> (rule1 % int3)) ((((triple2 triple3) -> (rule7 % int4))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Bob is not furry.
False
1
inv-proof
[(triple2 OR ((triple5) -> rule6))]
("Bob" "is" "furry" "-")
triple2
((triple5) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Anne is not round.
Unknown
inv-rconc
[@3: Anne is round.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule7 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is big.[(triple1)] Bob is furry.[(triple2 OR ((triple5) -> rule6))] Bob is green.[(triple3)] Bob is red.[(triple4 OR ((triple5) -> rule8) OR ((((((triple2 triple3) -> rule7)) -> rule5)) -> rule3) OR ((((((((triple5) -> rule6) triple3) -> rule7)) -> rule5)) -> rule3) OR ((((((((triple2 triple3) -> rule7)) -> rule1) ((((triple2 triple3) -> rule7)) -> rule5)) -> rule4)) -> rule8))] Bob is round.[(triple5 OR ((((((triple2 triple3) -> rule7)) -> rule1) ((((triple2 triple3) -> rule7)) -> rule5)) -> rule4))] Charlie is furry.[(triple6)] Charlie is green.[(triple7)] @1: Anne is red.[(((triple1) -> rule3))] Bob is quiet.[(((triple2 triple3) -> rule7) OR ((((triple5) -> rule6) triple3) -> rule7))] Charlie is quiet.[(((triple6 triple7) -> rule7))] @2: Bob is big.[(((((triple2 triple3) -> rule7)) -> rule5) OR ((((((triple5) -> rule6) triple3) -> rule7)) -> rule5))] Bob is kind.[(((((triple2 triple3) -> rule7)) -> rule1) OR ((((((triple5) -> rule6) triple3) -> rule7)) -> rule1))] Charlie is big.[(((((triple6 triple7) -> rule7)) -> rule5))] Charlie is kind.[(((((triple6 triple7) -> rule7)) -> rule1))] @3: Charlie is red.[(((((((triple6 triple7) -> rule7)) -> rule5)) -> rule3) OR ((((((((triple6 triple7) -> rule7)) -> rule1) ((((triple6 triple7) -> rule7)) -> rule5)) -> rule4)) -> rule8))] Charlie is round.[(((((((triple6 triple7) -> rule7)) -> rule1) ((((triple6 triple7) -> rule7)) -> rule5)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple5) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((triple5) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((((triple2 triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((((triple5) -> (rule6 % int4)) triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((((((triple2 triple3) -> (rule7 % int5))) -> (rule1 % int4)) ((((triple2 triple3) -> (rule7 % int5))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
int5
Bob is round.
("Bob" "is" "round" "+")
triple5
((((((triple2 triple3) -> (rule7 % int4))) -> (rule1 % int3)) ((((triple2 triple3) -> (rule7 % int4))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is green.
("Charlie" "is" "green" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2 triple3) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple5) -> (rule6 % int2)) triple3) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple6 triple7) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple2 triple3) -> (rule7 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple5) -> (rule6 % int3)) triple3) -> (rule7 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2 triple3) -> (rule7 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((((triple5) -> (rule6 % int3)) triple3) -> (rule7 % int2))) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
((((triple6 triple7) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple6 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple6 triple7) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((((triple6 triple7) -> (rule7 % int5))) -> (rule1 % int4)) ((((triple6 triple7) -> (rule7 % int5))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int5
Charlie is round.
("Charlie" "is" "round" "+")
((((((triple6 triple7) -> (rule7 % int4))) -> (rule1 % int3)) ((((triple6 triple7) -> (rule7 % int4))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4