The dog chases the squirrel. The squirrel chases the dog. The tiger eats the squirrel. If someone is blue and young then they chase the squirrel. If someone is cold and they chase the dog then the dog does not eat the squirrel. If someone eats the tiger then the tiger sees the dog. If someone eats the squirrel then they eat the tiger. If someone is red then they eat the tiger. If someone chases the squirrel and they eat the dog then the dog eats the tiger.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
If someone is blue and young then they chase the squirrel.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone is cold and they chase the dog then the dog does not eat the squirrel.
((("someone" "is" "cold" "+") ("someone" "chases" "dog" "+")) -> ("dog" "eats" "squirrel" "-"))
If someone eats the tiger then the tiger sees the dog.
((("someone" "eats" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If someone eats the squirrel then they eat the tiger.
((("someone" "eats" "squirrel" "+")) -> ("someone" "eats" "tiger" "+"))
If someone is red then they eat the tiger.
((("someone" "is" "red" "+")) -> ("someone" "eats" "tiger" "+"))
If someone chases the squirrel and they eat the dog then the dog eats the tiger.
((("someone" "chases" "squirrel" "+") ("someone" "eats" "dog" "+")) -> ("dog" "eats" "tiger" "+"))
The squirrel chases the dog.
True
1
proof
[(triple2)]
("squirrel" "chases" "dog" "+")
triple2
The dog does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "chases" "squirrel" "-")
triple1
The tiger eats the tiger.
True
2
proof
[(((triple3) -> rule4))]
("tiger" "eats" "tiger" "+")
((triple3) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple3) -> rule4))]
("tiger" "eats" "tiger" "-")
((triple3) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the dog.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("tiger" "sees" "dog" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger does not see the dog.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3))]
("tiger" "sees" "dog" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The squirrel does not eat the tiger.
Unknown
inv-rconc
[@1: The squirrel eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "eats" "tiger" "-")
The tiger chases the squirrel.
Unknown
rconc
[@1: The tiger chases the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "squirrel" "+")
The dog does not eat the tiger.
Unknown
inv-rconc
[@1: The dog eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "tiger" "-")
The dog eats the squirrel.
Unknown
random
[@0: The dog eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "squirrel" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The dog chases the squirrel.[(triple1)] The squirrel chases the dog.[(triple2)] The tiger eats the squirrel.[(triple3)] @1: The tiger eats the tiger.[(((triple3) -> rule4))] @2: The tiger sees the dog.[(((((triple3) -> rule4)) -> rule3))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple3
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple3) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2