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