Anne is blue. Anne is red. Bob is big. Bob is blue. Bob is red. Bob is young. Dave is big. Dave is cold. Dave is nice. Dave is red. Dave is young. Fiona is cold. Fiona is quiet. Fiona is red. Fiona is young. If Dave is red and Dave is cold then Dave is nice. Cold people are quiet. If Bob is red then Bob is cold. All blue, cold people are nice. All quiet, red people are cold. If someone is nice and blue then they are quiet. All young people are nice. If someone is red and blue then they are young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If Dave is red and Dave is cold then Dave is nice.
((("Dave" "is" "red" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "nice" "+"))
Cold people are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is red then Bob is cold.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "cold" "+"))
All blue, cold people are nice.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All quiet, red people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice and blue then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and blue then they are young.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Dave is big.
True
1
proof
[(triple7)]
("Dave" "is" "big" "+")
triple7
Dave is not young.
False
1
inv-proof
[(triple11)]
("Dave" "is" "young" "-")
triple11
Dave is quiet.
True
2
proof
[(((triple8) -> rule2))]
("Dave" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is not young.
False
3
inv-proof
[(((triple2 triple1) -> rule8))]
("Anne" "is" "young" "-")
((triple2 triple1) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is blue.[(triple1)] Anne is red.[(triple2)] Bob is big.[(triple3)] Bob is blue.[(triple4)] Bob is red.[(triple5)] Bob is young.[(triple6 OR ((triple5 triple4) -> rule8))] Dave is big.[(triple7)] Dave is cold.[(triple8)] Dave is nice.[(triple9 OR ((triple11) -> rule7) OR ((triple10 triple8) -> rule1))] Dave is red.[(triple10)] Dave is young.[(triple11)] Fiona is cold.[(triple12 OR ((triple13 triple14) -> rule5))] Fiona is quiet.[(triple13 OR ((triple12) -> rule2))] Fiona is red.[(triple14)] Fiona is young.[(triple15)] @1: Anne is young.[(((triple2 triple1) -> rule8))] Bob is cold.[(((triple5) -> rule3) OR ((((((triple6) -> rule7) triple4) -> rule6) triple5) -> rule5) OR ((((((((triple5 triple4) -> rule8)) -> rule7) triple4) -> rule6) triple5) -> rule5))] Bob is nice.[(((triple6) -> rule7) OR ((((triple5 triple4) -> rule8)) -> rule7) OR ((triple4 ((triple5) -> rule3)) -> rule4))] Dave is quiet.[(((triple8) -> rule2))] Fiona is nice.[(((triple15) -> rule7))] @2: Anne is nice.[(((((triple2 triple1) -> rule8)) -> rule7))] Bob is quiet.[(((((triple5) -> rule3)) -> rule2) OR ((((triple6) -> rule7) triple4) -> rule6) OR ((((((triple5 triple4) -> rule8)) -> rule7) triple4) -> rule6) OR ((((triple4 ((triple5) -> rule3)) -> rule4) triple4) -> rule6))] @3: Anne is quiet.[(((((((triple2 triple1) -> rule8)) -> rule7) triple1) -> rule6))] @4: Anne is cold.[(((((((((triple2 triple1) -> rule8)) -> rule7) triple1) -> rule6) triple2) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
((triple5 triple4) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
((triple11) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple10 triple8) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
Fiona is cold.
("Fiona" "is" "cold" "+")
triple12
((triple13 triple14) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple13
((triple12) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple14
Fiona is young.
("Fiona" "is" "young" "+")
triple15
Anne is young.
("Anne" "is" "young" "+")
((triple2 triple1) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple5) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((((triple6) -> (rule7 % int3)) triple4) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
((((((((triple5 triple4) -> (rule8 % int4))) -> (rule7 % int3)) triple4) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
((triple6) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple5 triple4) -> (rule8 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple4 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple15) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2 triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
((((triple6) -> (rule7 % int2)) triple4) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple5 triple4) -> (rule8 % int3))) -> (rule7 % int2)) triple4) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
((((triple4 ((triple5) -> (rule3 % int3))) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple2 triple1) -> (rule8 % int3))) -> (rule7 % int2)) triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
((((((((triple2 triple1) -> (rule8 % int4))) -> (rule7 % int3)) triple1) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4