Anne is big. Anne is nice. Anne is quiet. Anne is red. Anne is white. Dave is white. Fiona is big. Fiona is cold. Fiona is quiet. Fiona is white. If something is big then it is green. All white things are red. If something is cold then it is big. If something is red and white then it is cold. Cold things are white. If Dave is nice and Dave is quiet then Dave is big. If Dave is quiet and Dave is cold then Dave is white. All green things are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is red and white then it is cold.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If Dave is nice and Dave is quiet then Dave is big.
((("Dave" "is" "nice" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "big" "+"))
If Dave is quiet and Dave is cold then Dave is white.
((("Dave" "is" "quiet" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "white" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Anne is red.
True
1
proof
[(triple4 OR ((triple5) -> rule2) OR ((((triple1) -> rule1)) -> rule8))]
("Anne" "is" "red" "+")
triple4
((triple5) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not red.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule2) OR ((((triple1) -> rule1)) -> rule8))]
("Anne" "is" "red" "-")
triple4
((triple5) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Fiona is green.
True
2
proof
[(((triple7) -> rule1) OR ((((triple8) -> rule3)) -> rule1) OR ((((((((triple10) -> rule2) triple10) -> rule4)) -> rule3)) -> rule1))]
("Fiona" "is" "green" "+")
((triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((((((triple10) -> (rule2 % int4)) triple10) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Dave is not red.
False
2
inv-proof
[(((triple6) -> rule2))]
("Dave" "is" "red" "-")
((triple6) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is big.[(triple1 OR ((((triple4 triple5) -> rule4)) -> rule3) OR ((((((triple5) -> rule2) triple5) -> rule4)) -> rule3))] Anne is nice.[(triple2)] Anne is quiet.[(triple3)] Anne is red.[(triple4 OR ((triple5) -> rule2) OR ((((triple1) -> rule1)) -> rule8))] Anne is white.[(triple5)] Dave is white.[(triple6)] Fiona is big.[(triple7 OR ((triple8) -> rule3) OR ((((((triple10) -> rule2) triple10) -> rule4)) -> rule3))] Fiona is cold.[(triple8 OR ((((triple10) -> rule2) triple10) -> rule4) OR ((((((triple7) -> rule1)) -> rule8) triple10) -> rule4))] Fiona is quiet.[(triple9)] Fiona is white.[(triple10 OR ((triple8) -> rule5))] @1: Anne is cold.[(((triple4 triple5) -> rule4) OR ((((triple5) -> rule2) triple5) -> rule4) OR ((((((triple1) -> rule1)) -> rule8) triple5) -> rule4))] Anne is green.[(((triple1) -> rule1) OR ((((((triple4 triple5) -> rule4)) -> rule3)) -> rule1) OR ((((((((triple5) -> rule2) triple5) -> rule4)) -> rule3)) -> rule1))] Dave is red.[(((triple6) -> rule2))] Fiona is green.[(((triple7) -> rule1) OR ((((triple8) -> rule3)) -> rule1) OR ((((((((triple10) -> rule2) triple10) -> rule4)) -> rule3)) -> rule1))] Fiona is red.[(((triple10) -> rule2) OR ((((triple7) -> rule1)) -> rule8) OR ((((triple8) -> rule5)) -> rule2) OR ((((((triple8) -> rule3)) -> rule1)) -> rule8))] @2: Dave is cold.[(((((triple6) -> rule2) triple6) -> rule4))] @3: Dave is big.[(((((((triple6) -> rule2) triple6) -> rule4)) -> rule3))] @4: Dave is green.[(((((((((triple6) -> rule2) triple6) -> rule4)) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((((triple4 triple5) -> (rule4 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((((triple5) -> (rule2 % int3)) triple5) -> (rule4 % int2))) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple5) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Fiona is big.
("Fiona" "is" "big" "+")
triple7
((triple8) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((((triple10) -> (rule2 % int3)) triple10) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
((((triple10) -> (rule2 % int2)) triple10) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((((triple7) -> (rule1 % int3))) -> (rule8 % int2)) triple10) -> (rule4 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
((triple8) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((triple4 triple5) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple5) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple5) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((((triple4 triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((((triple5) -> (rule2 % int4)) triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
((triple6) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple7) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
((((((((triple10) -> (rule2 % int4)) triple10) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is red.
("Fiona" "is" "red" "+")
((triple10) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
((((((triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
((((triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple6) -> (rule2 % int3)) triple6) -> (rule4 % int2))) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
((((((((triple6) -> (rule2 % int4)) triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4