Bob is blue. Bob is furry. Bob is quiet. Bob is smart. Bob is white. Fiona is blue. Fiona is cold. Fiona is furry. Fiona is quiet. Fiona is white. If someone is smart and blue then they are cold. If someone is furry then they are quiet. If someone is quiet and furry then they are smart. If Bob is rough then Bob is white. If someone is rough then they are furry. All blue people are furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is smart and blue then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet and furry then they are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Bob is rough then Bob is white.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "white" "+"))
If someone is rough then they are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Fiona is furry.
True
1
proof
[(triple8 OR ((triple6) -> rule6))]
("Fiona" "is" "furry" "+")
triple8
((triple6) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Bob is not smart.
False
1
inv-proof
[(triple4 OR ((triple3 triple2) -> rule3) OR ((triple3 ((triple1) -> rule6)) -> rule3) OR ((((triple2) -> rule2) triple2) -> rule3) OR ((((triple2) -> rule2) ((triple1) -> rule6)) -> rule3) OR ((((((triple1) -> rule6)) -> rule2) triple2) -> rule3) OR ((((((triple1) -> rule6)) -> rule2) ((triple1) -> rule6)) -> rule3))]
("Bob" "is" "smart" "-")
triple4
((triple3 triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple2) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) ((triple1) -> (rule6 % int3))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2 OR ((triple1) -> rule6))] Bob is quiet.[(triple3 OR ((triple2) -> rule2) OR ((((triple1) -> rule6)) -> rule2))] Bob is smart.[(triple4 OR ((triple3 triple2) -> rule3) OR ((triple3 ((triple1) -> rule6)) -> rule3) OR ((((triple2) -> rule2) triple2) -> rule3) OR ((((triple2) -> rule2) ((triple1) -> rule6)) -> rule3) OR ((((((triple1) -> rule6)) -> rule2) triple2) -> rule3) OR ((((((triple1) -> rule6)) -> rule2) ((triple1) -> rule6)) -> rule3))] Bob is white.[(triple5)] Fiona is blue.[(triple6)] Fiona is cold.[(triple7 OR ((((triple9 triple8) -> rule3) triple6) -> rule1) OR ((((triple9 ((triple6) -> rule6)) -> rule3) triple6) -> rule1) OR ((((((triple8) -> rule2) triple8) -> rule3) triple6) -> rule1) OR ((((((triple8) -> rule2) ((triple6) -> rule6)) -> rule3) triple6) -> rule1) OR ((((((((triple6) -> rule6)) -> rule2) triple8) -> rule3) triple6) -> rule1) OR ((((((((triple6) -> rule6)) -> rule2) ((triple6) -> rule6)) -> rule3) triple6) -> rule1))] Fiona is furry.[(triple8 OR ((triple6) -> rule6))] Fiona is quiet.[(triple9 OR ((triple8) -> rule2) OR ((((triple6) -> rule6)) -> rule2))] Fiona is white.[(triple10)] @1: Bob is cold.[(((triple4 triple1) -> rule1) OR ((((triple3 triple2) -> rule3) triple1) -> rule1) OR ((((triple3 ((triple1) -> rule6)) -> rule3) triple1) -> rule1) OR ((((((triple2) -> rule2) triple2) -> rule3) triple1) -> rule1) OR ((((((triple2) -> rule2) ((triple1) -> rule6)) -> rule3) triple1) -> rule1) OR ((((((((triple1) -> rule6)) -> rule2) triple2) -> rule3) triple1) -> rule1) OR ((((((((triple1) -> rule6)) -> rule2) ((triple1) -> rule6)) -> rule3) triple1) -> rule1))] Fiona is smart.[(((triple9 triple8) -> rule3) OR ((triple9 ((triple6) -> rule6)) -> rule3) OR ((((triple8) -> rule2) triple8) -> rule3) OR ((((triple8) -> rule2) ((triple6) -> rule6)) -> rule3) OR ((((((triple6) -> rule6)) -> rule2) triple8) -> rule3) OR ((((((triple6) -> rule6)) -> rule2) ((triple6) -> rule6)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple1) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
((triple2) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((triple3 triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple3 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple2) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple2) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) ((triple1) -> (rule6 % int3))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
((((triple9 triple8) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple9 ((triple6) -> (rule6 % int3))) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple8) -> (rule2 % int3)) triple8) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((((triple8) -> (rule2 % int4)) ((triple6) -> (rule6 % int3))) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
((((((((triple6) -> (rule6 % int4))) -> (rule2 % int3)) triple8) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
((((((((triple6) -> (rule6 % int4))) -> (rule2 % int3)) ((triple6) -> (rule6 % int4))) -> (rule3 % int2)) triple6) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
((triple6) -> (rule6 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
((triple8) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Bob is cold.
("Bob" "is" "cold" "+")
((triple4 triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple3 triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple3 ((triple1) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple2) -> (rule2 % int3)) triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((((triple2) -> (rule2 % int4)) ((triple1) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
((((((((triple1) -> (rule6 % int4))) -> (rule2 % int3)) triple2) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
((((((((triple1) -> (rule6 % int4))) -> (rule2 % int3)) ((triple1) -> (rule6 % int4))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple9 triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple9 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple8) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple8) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2)) triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2)) ((triple6) -> (rule6 % int3))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3