The dog needs the squirrel. The mouse visits the tiger. The squirrel visits the dog. The tiger is round. If someone visits the dog then the dog needs the mouse. If someone needs the squirrel then the squirrel is cold. If the tiger is cold and the tiger sees the dog then the tiger visits the mouse. If someone visits the dog and the dog sees the squirrel then the dog sees the mouse. If someone needs the squirrel and they need the mouse then they are cold. If someone sees the squirrel and the squirrel is cold then the squirrel sees the dog.
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone visits the dog then the dog needs the mouse.
((("someone" "visits" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If someone needs the squirrel then the squirrel is cold.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If the tiger is cold and the tiger sees the dog then the tiger visits the mouse.
((("tiger" "is" "cold" "+") ("tiger" "sees" "dog" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone visits the dog and the dog sees the squirrel then the dog sees the mouse.
((("someone" "visits" "dog" "+") ("dog" "sees" "squirrel" "+")) -> ("dog" "sees" "mouse" "+"))
If someone needs the squirrel and they need the mouse then they are cold.
((("someone" "needs" "squirrel" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the squirrel and the squirrel is cold then the squirrel sees the dog.
((("someone" "sees" "squirrel" "+") ("squirrel" "is" "cold" "+")) -> ("squirrel" "sees" "dog" "+"))
The squirrel visits the dog.
True
1
proof
[(triple3)]
("squirrel" "visits" "dog" "+")
triple3
The tiger is not round.
False
1
inv-proof
[(triple4)]
("tiger" "is" "round" "-")
triple4
The squirrel is cold.
True
2
proof
[(((triple1) -> rule2))]
("squirrel" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The dog does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "needs" "mouse" "-")
((triple3) -> (rule1 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog is cold.
True
4
proof
[(((triple1 ((triple3) -> rule1)) -> rule5))]
("dog" "is" "cold" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The dog is not cold.
False
4
inv-proof
[(((triple1 ((triple3) -> rule1)) -> rule5))]
("dog" "is" "cold" "-")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "cold" "-")
The dog sees the mouse.
Unknown
rconc
[@1: The dog sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "sees" "mouse" "+")
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "cold" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
The tiger does not see the dog.
Unknown
inv-random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "-")
The squirrel sees the tiger.
Unknown
random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "+")
@0: The dog needs the squirrel.[(triple1)] The mouse visits the tiger.[(triple2)] The squirrel visits the dog.[(triple3)] The tiger is round.[(triple4)] @1: The dog needs the mouse.[(((triple3) -> rule1))] The squirrel is cold.[(((triple1) -> rule2))] @2: The dog is cold.[(((triple1 ((triple3) -> rule1)) -> rule5))]
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple3
The tiger is round.
("tiger" "is" "round" "+")
triple4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple3) -> (rule1 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2