Bob is blue. Bob is cold. Bob is nice. Bob is quiet. Bob is round. Bob is white. Dave is blue. Dave is green. Dave is quiet. Dave is round. Dave is white. Fiona is cold. Fiona is nice. Fiona is round. Fiona is white. If Fiona is blue and Fiona is cold then Fiona is white. If something is nice and round then it is white. White, round things are cold. If something is nice and blue then it is round. If Fiona is quiet then Fiona is cold. All quiet things are cold. If something is nice and quiet then it is cold. Green things are white.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If Fiona is blue and Fiona is cold then Fiona is white.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "white" "+"))
If something is nice and round then it is white.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
White, round things are cold.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is nice and blue then it is round.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Fiona is quiet then Fiona is cold.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "cold" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is nice and quiet then it is cold.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
Bob is quiet.
True
1
proof
[(triple4)]
("Bob" "is" "quiet" "+")
triple4
Fiona is not nice.
False
1
inv-proof
[(triple13)]
("Fiona" "is" "nice" "-")
triple13
Dave is cold.
True
2
proof
[(((triple9) -> rule6) OR ((triple11 triple10) -> rule3) OR ((((triple8) -> rule8) triple10) -> rule3))]
("Dave" "is" "cold" "+")
((triple9) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple11 triple10) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple8) -> (rule8 % int2)) triple10) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not cold.
False
2
inv-proof
[(((triple9) -> rule6) OR ((triple11 triple10) -> rule3) OR ((((triple8) -> rule8) triple10) -> rule3))]
("Dave" "is" "cold" "-")
((triple9) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple11 triple10) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple8) -> (rule8 % int2)) triple10) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple4) -> rule6) OR ((triple3 triple4) -> rule7) OR ((triple6 triple5) -> rule3) OR ((triple6 ((triple3 triple1) -> rule4)) -> rule3) OR ((((triple3 triple5) -> rule2) triple5) -> rule3) OR ((((triple3 triple5) -> rule2) ((triple3 triple1) -> rule4)) -> rule3) OR ((((triple3 ((triple3 triple1) -> rule4)) -> rule2) triple5) -> rule3) OR ((((triple3 ((triple3 triple1) -> rule4)) -> rule2) ((triple3 triple1) -> rule4)) -> rule3))] Bob is nice.[(triple3)] Bob is quiet.[(triple4)] Bob is round.[(triple5 OR ((triple3 triple1) -> rule4))] Bob is white.[(triple6 OR ((triple3 triple5) -> rule2) OR ((triple3 ((triple3 triple1) -> rule4)) -> rule2))] Dave is blue.[(triple7)] Dave is green.[(triple8)] Dave is quiet.[(triple9)] Dave is round.[(triple10)] Dave is white.[(triple11 OR ((triple8) -> rule8))] Fiona is cold.[(triple12 OR ((triple15 triple14) -> rule3) OR ((((triple13 triple14) -> rule2) triple14) -> rule3))] Fiona is nice.[(triple13)] Fiona is round.[(triple14)] Fiona is white.[(triple15 OR ((triple13 triple14) -> rule2))] @1: Dave is cold.[(((triple9) -> rule6) OR ((triple11 triple10) -> rule3) OR ((((triple8) -> rule8) triple10) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple4) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple3 triple4) -> (rule7 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6 triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple6 ((triple3 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple3 triple5) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple3 triple5) -> (rule2 % int3)) ((triple3 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((((triple3 ((triple3 triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((triple3 ((triple3 triple1) -> (rule4 % int3))) -> (rule2 % int2)) ((triple3 triple1) -> (rule4 % int3))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple3 triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple3 triple5) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple3 ((triple3 triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
((triple8) -> (rule8 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple12
((triple15 triple14) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
((((triple13 triple14) -> (rule2 % int2)) triple14) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
Fiona is round.
("Fiona" "is" "round" "+")
triple14
Fiona is white.
("Fiona" "is" "white" "+")
triple15
((triple13 triple14) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple9) -> (rule6 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple11 triple10) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple8) -> (rule8 % int2)) triple10) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2