Anne is quiet. Anne is rough. Anne is smart. Bob is green. Bob is red. Bob is rough. Bob is smart. Fiona is big. Fiona is red. Gary is furry. Gary is red. Gary is rough. If Bob is quiet then Bob is red. Quiet things are green. All smart, big things are quiet. All big, green things are furry. If Bob is red then Bob is big. If something is rough and red then it is smart. If Bob is green then Bob is red. Smart, rough things are red.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Bob is quiet then Bob is red.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "red" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
All smart, big things are quiet.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All big, green things are furry.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
If Bob is red then Bob is big.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "big" "+"))
If something is rough and red then it is smart.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Bob is green then Bob is red.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "red" "+"))
Smart, rough things are red.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Gary is rough.
True
1
proof
[(triple12)]
("Gary" "is" "rough" "+")
triple12
Anne is not rough.
False
1
inv-proof
[(triple2)]
("Anne" "is" "rough" "-")
triple2
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Anne is quiet.[(triple1)] Anne is rough.[(triple2)] Anne is smart.[(triple3)] Bob is green.[(triple4 OR ((((triple7 ((triple5) -> rule5)) -> rule3)) -> rule2) OR ((((((triple6 triple5) -> rule6) ((triple5) -> rule5)) -> rule3)) -> rule2) OR ((((triple7 ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3)) -> rule2) OR ((((((triple6 triple5) -> rule6) ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3)) -> rule2))] Bob is red.[(triple5 OR ((triple4) -> rule7) OR ((triple7 triple6) -> rule8))] Bob is rough.[(triple6)] Bob is smart.[(triple7 OR ((triple6 triple5) -> rule6) OR ((triple6 ((triple4) -> rule7)) -> rule6))] Fiona is big.[(triple8)] Fiona is red.[(triple9)] Gary is furry.[(triple10)] Gary is red.[(triple11)] Gary is rough.[(triple12)] @1: Anne is green.[(((triple1) -> rule2))] Anne is red.[(((triple3 triple2) -> rule8))] Bob is big.[(((triple5) -> rule5) OR ((((triple4) -> rule7)) -> rule5) OR ((((triple7 triple6) -> rule8)) -> rule5))] Gary is smart.[(((triple12 triple11) -> rule6))] @2: Bob is furry.[(((((triple5) -> rule5) triple4) -> rule4) OR ((((((triple4) -> rule7)) -> rule5) triple4) -> rule4) OR ((((((triple7 triple6) -> rule8)) -> rule5) triple4) -> rule4) OR ((((triple5) -> rule5) ((((triple7 ((triple5) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((triple5) -> rule5) ((((((triple6 triple5) -> rule6) ((triple5) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule7)) -> rule5) ((((triple7 ((triple5) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple7 triple6) -> rule8)) -> rule5) ((((triple7 ((triple5) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule7)) -> rule5) ((((((triple6 triple5) -> rule6) ((triple5) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple7 triple6) -> rule8)) -> rule5) ((((((triple6 triple5) -> rule6) ((triple5) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((triple5) -> rule5) ((((triple7 ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((triple5) -> rule5) ((((((triple6 triple5) -> rule6) ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule7)) -> rule5) ((((triple7 ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple7 triple6) -> rule8)) -> rule5) ((((triple7 ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule7)) -> rule5) ((((((triple6 triple5) -> rule6) ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3)) -> rule2)) -> rule4) OR ((((((triple7 triple6) -> rule8)) -> rule5) ((((((triple6 triple5) -> rule6) ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3)) -> rule2)) -> rule4))] Bob is quiet.[(((triple7 ((triple5) -> rule5)) -> rule3) OR ((((triple6 triple5) -> rule6) ((triple5) -> rule5)) -> rule3) OR ((triple7 ((((triple4) -> rule7)) -> rule5)) -> rule3) OR ((triple7 ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3) OR ((((triple6 triple5) -> rule6) ((((triple4) -> rule7)) -> rule5)) -> rule3) OR ((((triple6 triple5) -> rule6) ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3) OR ((((triple6 ((triple4) -> rule7)) -> rule6) ((triple5) -> rule5)) -> rule3) OR ((((triple6 ((triple4) -> rule7)) -> rule6) ((((triple4) -> rule7)) -> rule5)) -> rule3) OR ((((triple6 ((triple4) -> rule7)) -> rule6) ((((triple7 triple6) -> rule8)) -> rule5)) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
((((triple7 ((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple6 triple5) -> (rule6 % int4)) ((triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((triple7 ((((triple7 triple6) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((((((triple6 triple5) -> (rule6 % int5)) ((((triple7 triple6) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple4) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple7 triple6) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((triple6 triple5) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple6 ((triple4) -> (rule7 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple3 triple2) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple5) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple7 triple6) -> (rule8 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple12 triple11) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple5) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple4) -> (rule7 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((((triple7 triple6) -> (rule8 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple5) -> (rule5 % int4)) ((((triple7 ((triple5) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
((((triple5) -> (rule5 % int5)) ((((((triple6 triple5) -> (rule6 % int4)) ((triple5) -> (rule5 % int5))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
((((((triple4) -> (rule7 % int5))) -> (rule5 % int4)) ((((triple7 ((triple5) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
((((((triple7 triple6) -> (rule8 % int5))) -> (rule5 % int4)) ((((triple7 ((triple5) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
((((((triple4) -> (rule7 % int6))) -> (rule5 % int5)) ((((((triple6 triple5) -> (rule6 % int4)) ((triple5) -> (rule5 % int5))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
int6
((((((triple7 triple6) -> (rule8 % int6))) -> (rule5 % int5)) ((((((triple6 triple5) -> (rule6 % int4)) ((triple5) -> (rule5 % int5))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
int6
((((triple5) -> (rule5 % int5)) ((((triple7 ((((triple7 triple6) -> (rule8 % int4))) -> (rule5 % int5))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
((((triple5) -> (rule5 % int6)) ((((((triple6 triple5) -> (rule6 % int5)) ((((triple7 triple6) -> (rule8 % int4))) -> (rule5 % int6))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Bob is big.
("Bob" "is" "big" "+")
int6
((((((triple4) -> (rule7 % int5))) -> (rule5 % int4)) ((((triple7 ((((triple7 triple6) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
((((((triple7 triple6) -> (rule8 % int5))) -> (rule5 % int4)) ((((triple7 ((((triple7 triple6) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is big.
("Bob" "is" "big" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
((((((triple4) -> (rule7 % int6))) -> (rule5 % int5)) ((((((triple6 triple5) -> (rule6 % int4)) ((((triple7 triple6) -> (rule8 % int6))) -> (rule5 % int5))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
int6
((((((triple7 triple6) -> (rule8 % int6))) -> (rule5 % int5)) ((((((triple6 triple5) -> (rule6 % int4)) ((((triple7 triple6) -> (rule8 % int6))) -> (rule5 % int5))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is big.
("Bob" "is" "big" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
int6
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple7 ((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple6 triple5) -> (rule6 % int3)) ((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((triple7 ((((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((triple7 ((((triple7 triple6) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple6 triple5) -> (rule6 % int4)) ((((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((triple6 triple5) -> (rule6 % int4)) ((((triple7 triple6) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((triple6 ((triple4) -> (rule7 % int4))) -> (rule6 % int3)) ((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((((triple6 ((triple4) -> (rule7 % int4))) -> (rule6 % int3)) ((((triple4) -> (rule7 % int4))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((((triple6 ((triple4) -> (rule7 % int4))) -> (rule6 % int3)) ((((triple7 triple6) -> (rule8 % int4))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4