The dog needs the tiger. The squirrel needs the dog. The tiger visits the squirrel. If someone needs the tiger then the tiger chases the squirrel. If someone needs the squirrel then the squirrel visits the dog. If someone chases the squirrel then the squirrel visits the tiger.
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone needs the tiger then the tiger chases the squirrel.
((("someone" "needs" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
If someone needs the squirrel then the squirrel visits the dog.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "visits" "dog" "+"))
If someone chases the squirrel then the squirrel visits the tiger.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "visits" "tiger" "+"))
The dog needs the tiger.
True
1
proof
[(triple1)]
("dog" "needs" "tiger" "+")
triple1
The squirrel does not need the dog.
False
1
inv-proof
[(triple2)]
("squirrel" "needs" "dog" "-")
triple2
The tiger chases the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "chases" "squirrel" "+")
((triple1) -> (rule1 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger does not chase the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("tiger" "chases" "squirrel" "-")
((triple1) -> (rule1 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel visits the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("squirrel" "visits" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The squirrel does not visit the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("squirrel" "visits" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2
The squirrel does not visit the dog.
Unknown
inv-rconc
[@1: The squirrel visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "dog" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The dog visits the squirrel.
Unknown
random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The dog needs the tiger.[(triple1)] The squirrel needs the dog.[(triple2)] The tiger visits the squirrel.[(triple3)] @1: The tiger chases the squirrel.[(((triple1) -> rule1))] @2: The squirrel visits the tiger.[(((((triple1) -> rule1)) -> rule3))]
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((triple1) -> (rule1 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int2