Charlie is blue. Charlie is cold. Charlie is red. Erin is big. Erin is cold. Erin is quiet. Erin is red. Erin is round. Fiona is big. Fiona is quiet. Fiona is red. Fiona is round. All quiet, cold things are round. Big things are blue. If something is quiet then it is round. If something is round and blue then it is smart. All smart, blue things are red. If something is big and quiet then it is red. If Erin is quiet then Erin is blue. If Erin is round then Erin is smart.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
All quiet, cold things are round.
((("something" "is" "quiet" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is quiet then it is round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is round and blue then it is smart.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All smart, blue things are red.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is big and quiet then it is red.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Erin is quiet then Erin is blue.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "blue" "+"))
If Erin is round then Erin is smart.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "smart" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple6)]
("Erin" "is" "quiet" "-")
triple6
Erin is blue.
True
2
proof
[(((triple4) -> rule2) OR ((triple6) -> rule7))]
("Erin" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple6) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple8) -> rule8) OR ((((triple6) -> rule3)) -> rule8) OR ((((triple6 triple5) -> rule1)) -> rule8) OR ((triple8 ((triple4) -> rule2)) -> rule4) OR ((triple8 ((triple6) -> rule7)) -> rule4) OR ((((triple6) -> rule3) ((triple4) -> rule2)) -> rule4) OR ((((triple6) -> rule3) ((triple6) -> rule7)) -> rule4) OR ((((triple6 triple5) -> rule1) ((triple4) -> rule2)) -> rule4) OR ((((triple6 triple5) -> rule1) ((triple6) -> rule7)) -> rule4))]
("Erin" "is" "smart" "-")
((triple8) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple6 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((triple8 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((triple8 ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple6) -> (rule3 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple6) -> (rule3 % int3)) ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple6 triple5) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple6 triple5) -> (rule1 % int3)) ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Fiona is smart.
True
4
proof
[(((triple12 ((triple9) -> rule2)) -> rule4) OR ((((triple10) -> rule3) ((triple9) -> rule2)) -> rule4))]
("Fiona" "is" "smart" "+")
((triple12 ((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is not smart.
False
4
inv-proof
[(((triple12 ((triple9) -> rule2)) -> rule4) OR ((((triple10) -> rule3) ((triple9) -> rule2)) -> rule4))]
("Fiona" "is" "smart" "-")
((triple12 ((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is red.[(triple3)] Erin is big.[(triple4)] Erin is cold.[(triple5)] Erin is quiet.[(triple6)] Erin is red.[(triple7 OR ((triple4 triple6) -> rule6) OR ((((triple8) -> rule8) ((triple4) -> rule2)) -> rule5) OR ((((triple8) -> rule8) ((triple6) -> rule7)) -> rule5) OR ((((((triple6) -> rule3)) -> rule8) ((triple4) -> rule2)) -> rule5) OR ((((((triple6) -> rule3)) -> rule8) ((triple6) -> rule7)) -> rule5) OR ((((((triple6 triple5) -> rule1)) -> rule8) ((triple4) -> rule2)) -> rule5) OR ((((((triple6 triple5) -> rule1)) -> rule8) ((triple6) -> rule7)) -> rule5) OR ((((triple8 ((triple4) -> rule2)) -> rule4) ((triple4) -> rule2)) -> rule5) OR ((((triple8 ((triple4) -> rule2)) -> rule4) ((triple6) -> rule7)) -> rule5) OR ((((triple8 ((triple6) -> rule7)) -> rule4) ((triple4) -> rule2)) -> rule5) OR ((((triple8 ((triple6) -> rule7)) -> rule4) ((triple6) -> rule7)) -> rule5) OR ((((((triple6) -> rule3) ((triple4) -> rule2)) -> rule4) ((triple4) -> rule2)) -> rule5) OR ((((((triple6) -> rule3) ((triple4) -> rule2)) -> rule4) ((triple6) -> rule7)) -> rule5) OR ((((((triple6) -> rule3) ((triple6) -> rule7)) -> rule4) ((triple4) -> rule2)) -> rule5) OR ((((((triple6) -> rule3) ((triple6) -> rule7)) -> rule4) ((triple6) -> rule7)) -> rule5) OR ((((((triple6 triple5) -> rule1) ((triple4) -> rule2)) -> rule4) ((triple4) -> rule2)) -> rule5) OR ((((((triple6 triple5) -> rule1) ((triple4) -> rule2)) -> rule4) ((triple6) -> rule7)) -> rule5) OR ((((((triple6 triple5) -> rule1) ((triple6) -> rule7)) -> rule4) ((triple4) -> rule2)) -> rule5) OR ((((((triple6 triple5) -> rule1) ((triple6) -> rule7)) -> rule4) ((triple6) -> rule7)) -> rule5))] Erin is round.[(triple8 OR ((triple6) -> rule3) OR ((triple6 triple5) -> rule1))] Fiona is big.[(triple9)] Fiona is quiet.[(triple10)] Fiona is red.[(triple11 OR ((triple9 triple10) -> rule6) OR ((((triple12 ((triple9) -> rule2)) -> rule4) ((triple9) -> rule2)) -> rule5) OR ((((((triple10) -> rule3) ((triple9) -> rule2)) -> rule4) ((triple9) -> rule2)) -> rule5))] Fiona is round.[(triple12 OR ((triple10) -> rule3))] @1: Erin is blue.[(((triple4) -> rule2) OR ((triple6) -> rule7))] Erin is smart.[(((triple8) -> rule8) OR ((((triple6) -> rule3)) -> rule8) OR ((((triple6 triple5) -> rule1)) -> rule8) OR ((triple8 ((triple4) -> rule2)) -> rule4) OR ((triple8 ((triple6) -> rule7)) -> rule4) OR ((((triple6) -> rule3) ((triple4) -> rule2)) -> rule4) OR ((((triple6) -> rule3) ((triple6) -> rule7)) -> rule4) OR ((((triple6 triple5) -> rule1) ((triple4) -> rule2)) -> rule4) OR ((((triple6 triple5) -> rule1) ((triple6) -> rule7)) -> rule4))] Fiona is blue.[(((triple9) -> rule2))] @2: Fiona is smart.[(((triple12 ((triple9) -> rule2)) -> rule4) OR ((((triple10) -> rule3) ((triple9) -> rule2)) -> rule4))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
((triple4 triple6) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple8) -> (rule8 % int3)) ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple8) -> (rule8 % int3)) ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple6) -> (rule3 % int4))) -> (rule8 % int3)) ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6) -> (rule3 % int4))) -> (rule8 % int3)) ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6 triple5) -> (rule1 % int4))) -> (rule8 % int3)) ((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6 triple5) -> (rule1 % int4))) -> (rule8 % int3)) ((triple6) -> (rule7 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((triple8 ((triple4) -> (rule2 % int3))) -> (rule4 % int2)) ((triple4) -> (rule2 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((triple8 ((triple4) -> (rule2 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((triple8 ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) ((triple4) -> (rule2 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((triple8 ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple6) -> (rule3 % int4)) ((triple4) -> (rule2 % int3))) -> (rule4 % int2)) ((triple4) -> (rule2 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6) -> (rule3 % int4)) ((triple4) -> (rule2 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6) -> (rule3 % int4)) ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) ((triple4) -> (rule2 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6) -> (rule3 % int4)) ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6 triple5) -> (rule1 % int4)) ((triple4) -> (rule2 % int3))) -> (rule4 % int2)) ((triple4) -> (rule2 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6 triple5) -> (rule1 % int4)) ((triple4) -> (rule2 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6 triple5) -> (rule1 % int4)) ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) ((triple4) -> (rule2 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((triple6 triple5) -> (rule1 % int4)) ((triple6) -> (rule7 % int3))) -> (rule4 % int2)) ((triple6) -> (rule7 % int3))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is round.
("Erin" "is" "round" "+")
triple8
((triple6) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple6 triple5) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple9
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
Fiona is red.
("Fiona" "is" "red" "+")
triple11
((triple9 triple10) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple12 ((triple9) -> (rule2 % int3))) -> (rule4 % int2)) ((triple9) -> (rule2 % int3))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
((((((triple10) -> (rule3 % int4)) ((triple9) -> (rule2 % int3))) -> (rule4 % int2)) ((triple9) -> (rule2 % int3))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
triple12
((triple10) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple6) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple8) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple6 triple5) -> (rule1 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((triple8 ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((triple8 ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((triple6) -> (rule3 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple6) -> (rule3 % int3)) ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple6 triple5) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple6 triple5) -> (rule1 % int3)) ((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple9) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple12 ((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple9) -> (rule2 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3