Anne is blue. Anne is green. Anne is red. Anne is smart. Erin is big. Erin is blue. Erin is cold. Erin is white. Harry is big. Harry is cold. All blue people are smart. All smart people are cold. If someone is red then they are smart. Blue, white people are big. If someone is big then they are white. All smart people are blue. If someone is green then they are blue. Smart, cold people are green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Blue, white people are big.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All smart people are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Smart, cold people are green.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Harry is big.
True
1
proof
[(triple9)]
("Harry" "is" "big" "+")
triple9
Anne is not blue.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule7) OR ((triple4) -> rule6) OR ((((triple3) -> rule3)) -> rule6) OR ((((triple4 ((triple4) -> rule2)) -> rule8)) -> rule7) OR ((((((triple3) -> rule3) ((triple4) -> rule2)) -> rule8)) -> rule7) OR ((((triple4 ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule7) OR ((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule7))]
("Anne" "is" "blue" "-")
triple1
((triple2) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple4) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple4 ((triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple3) -> (rule3 % int4)) ((triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
((((triple4 ((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
((((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Harry is not green.
Unknown
inv-rconc
[@4: Harry is green.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule6 <- rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is blue.[(triple1 OR ((triple2) -> rule7) OR ((triple4) -> rule6) OR ((((triple3) -> rule3)) -> rule6) OR ((((triple4 ((triple4) -> rule2)) -> rule8)) -> rule7) OR ((((((triple3) -> rule3) ((triple4) -> rule2)) -> rule8)) -> rule7) OR ((((triple4 ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule7) OR ((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8)) -> rule7))] Anne is green.[(triple2 OR ((triple4 ((triple4) -> rule2)) -> rule8) OR ((((triple1) -> rule1) ((triple4) -> rule2)) -> rule8) OR ((((triple3) -> rule3) ((triple4) -> rule2)) -> rule8) OR ((triple4 ((((triple1) -> rule1)) -> rule2)) -> rule8) OR ((triple4 ((((triple3) -> rule3)) -> rule2)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule8) OR ((((triple1) -> rule1) ((((triple3) -> rule3)) -> rule2)) -> rule8) OR ((((triple3) -> rule3) ((((triple1) -> rule1)) -> rule2)) -> rule8) OR ((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule2)) -> rule8))] Anne is red.[(triple3)] Anne is smart.[(triple4 OR ((triple1) -> rule1) OR ((triple3) -> rule3) OR ((((triple2) -> rule7)) -> rule1))] Erin is big.[(triple5 OR ((triple6 triple8) -> rule4))] Erin is blue.[(triple6)] Erin is cold.[(triple7 OR ((((triple6) -> rule1)) -> rule2))] Erin is white.[(triple8 OR ((triple5) -> rule5))] Harry is big.[(triple9)] Harry is cold.[(triple10)] @1: Anne is cold.[(((triple4) -> rule2) OR ((((triple1) -> rule1)) -> rule2) OR ((((triple3) -> rule3)) -> rule2) OR ((((((triple2) -> rule7)) -> rule1)) -> rule2))] Erin is smart.[(((triple6) -> rule1))] Harry is white.[(((triple9) -> rule5))] @2: Erin is green.[(((((triple6) -> rule1) triple7) -> rule8) OR ((((triple6) -> rule1) ((((triple6) -> rule1)) -> rule2)) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple4) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple4 ((triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple3) -> (rule3 % int4)) ((triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
((((triple4 ((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
((((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple4 ((triple4) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple4) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple4) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((triple4 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((triple4 ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((triple3) -> (rule3 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple3) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple5
((triple6 triple8) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple8
((triple5) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
Anne is cold.
("Anne" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((triple6) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple9) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple6) -> (rule1 % int3)) ((((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3