The dog eats the mouse. The dog is cold. The dog is nice. The dog is red. The dog needs the mouse. The dog visits the mouse. The mouse is red. If someone is blue then they need the mouse. If someone needs the mouse and the mouse is young then they are cold. If someone is blue and nice then they need the mouse. If the mouse needs the dog and the mouse visits the dog then the dog needs the mouse. If someone is young then they visit the mouse. If someone needs the mouse and they are cold then the mouse is young. Nice people are blue. If someone visits the mouse then the mouse eats the dog.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse is red.
("mouse" "is" "red" "+")
If someone is blue then they need the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the mouse and the mouse is young then they are cold.
((("someone" "needs" "mouse" "+") ("mouse" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue and nice then they need the mouse.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "mouse" "+"))
If the mouse needs the dog and the mouse visits the dog then the dog needs the mouse.
((("mouse" "needs" "dog" "+") ("mouse" "visits" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If someone is young then they visit the mouse.
((("someone" "is" "young" "+")) -> ("someone" "visits" "mouse" "+"))
If someone needs the mouse and they are cold then the mouse is young.
((("someone" "needs" "mouse" "+") ("someone" "is" "cold" "+")) -> ("mouse" "is" "young" "+"))
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone visits the mouse then the mouse eats the dog.
((("someone" "visits" "mouse" "+")) -> ("mouse" "eats" "dog" "+"))
The dog visits the mouse.
True
1
proof
[(triple6)]
("dog" "visits" "mouse" "+")
triple6
The dog does not need the mouse.
False
1
inv-proof
[(triple5 OR ((((triple3) -> rule7)) -> rule1) OR ((((triple3) -> rule7) triple3) -> rule3))]
("dog" "needs" "mouse" "-")
triple5
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple3) -> (rule7 % int2)) triple3) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog is blue.
True
2
proof
[(((triple3) -> rule7))]
("dog" "is" "blue" "+")
((triple3) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not blue.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "is" "blue" "-")
((triple3) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The mouse visits the mouse.
True
4
proof
[(((((triple5 triple2) -> rule6)) -> rule5) OR ((((((((triple3) -> rule7)) -> rule1) triple2) -> rule6)) -> rule5) OR ((((((((triple3) -> rule7) triple3) -> rule3) triple2) -> rule6)) -> rule5))]
("mouse" "visits" "mouse" "+")
((((triple5 triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((((((triple3) -> (rule7 % int4))) -> (rule1 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4
((((((((triple3) -> (rule7 % int4)) triple3) -> (rule3 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4
The mouse does not visit the mouse.
False
4
inv-proof
[(((((triple5 triple2) -> rule6)) -> rule5) OR ((((((((triple3) -> rule7)) -> rule1) triple2) -> rule6)) -> rule5) OR ((((((((triple3) -> rule7) triple3) -> rule3) triple2) -> rule6)) -> rule5))]
("mouse" "visits" "mouse" "-")
((((triple5 triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((((((triple3) -> (rule7 % int4))) -> (rule1 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4
((((((((triple3) -> (rule7 % int4)) triple3) -> (rule3 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4
The mouse is not cold.
Unknown
inv-rconc
[@3: The mouse is cold.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule7 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse needs the mouse.
Unknown
rconc
[@2: The mouse needs the mouse.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "is" "blue" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The dog eats the mouse.[(triple1)] The dog is cold.[(triple2)] The dog is nice.[(triple3)] The dog is red.[(triple4)] The dog needs the mouse.[(triple5 OR ((((triple3) -> rule7)) -> rule1) OR ((((triple3) -> rule7) triple3) -> rule3))] The dog visits the mouse.[(triple6)] The mouse is red.[(triple7)] @1: The dog is blue.[(((triple3) -> rule7))] The mouse eats the dog.[(((triple6) -> rule8) OR ((((((triple5 triple2) -> rule6)) -> rule5)) -> rule8) OR ((((((((((triple3) -> rule7)) -> rule1) triple2) -> rule6)) -> rule5)) -> rule8) OR ((((((((((triple3) -> rule7) triple3) -> rule3) triple2) -> rule6)) -> rule5)) -> rule8))] The mouse is young.[(((triple5 triple2) -> rule6) OR ((((((triple3) -> rule7)) -> rule1) triple2) -> rule6) OR ((((((triple3) -> rule7) triple3) -> rule3) triple2) -> rule6))] @2: The mouse visits the mouse.[(((((triple5 triple2) -> rule6)) -> rule5) OR ((((((((triple3) -> rule7)) -> rule1) triple2) -> rule6)) -> rule5) OR ((((((((triple3) -> rule7) triple3) -> rule3) triple2) -> rule6)) -> rule5))]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple5
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple3) -> (rule7 % int2)) triple3) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The dog is blue.
("dog" "is" "blue" "+")
((triple3) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((triple6) -> (rule8 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
((((((triple5 triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
((((((((((triple3) -> (rule7 % int5))) -> (rule1 % int4)) triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int4
The dog is blue.
("dog" "is" "blue" "+")
int5
((((((((((triple3) -> (rule7 % int5)) triple3) -> (rule3 % int4)) triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int4
The dog is blue.
("dog" "is" "blue" "+")
int5
The mouse is young.
("mouse" "is" "young" "+")
((triple5 triple2) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
((((((triple3) -> (rule7 % int3)) triple3) -> (rule3 % int2)) triple2) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((triple5 triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((((((triple3) -> (rule7 % int4))) -> (rule1 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4
((((((((triple3) -> (rule7 % int4)) triple3) -> (rule3 % int3)) triple2) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int3
The dog is blue.
("dog" "is" "blue" "+")
int4