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