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