The cow is round. The dog needs the cow. The squirrel needs the tiger. The tiger needs the squirrel. If the cow is cold then the cow visits the dog. If something needs the tiger and the tiger needs the cow then the tiger is not young. If something visits the squirrel then it does not see the dog. If something needs the squirrel then it visits the squirrel. If the dog is green then the dog sees the squirrel. Round, cold things are not young. If something is red then it does not need the dog. If something needs the squirrel then the squirrel sees the cow.
The cow is round.
("cow" "is" "round" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If the cow is cold then the cow visits the dog.
((("cow" "is" "cold" "+")) -> ("cow" "visits" "dog" "+"))
If something needs the tiger and the tiger needs the cow then the tiger is not young.
((("something" "needs" "tiger" "+") ("tiger" "needs" "cow" "+")) -> ("tiger" "is" "young" "-"))
If something visits the squirrel then it does not see the dog.
((("something" "visits" "squirrel" "+")) -> ("something" "sees" "dog" "-"))
If something needs the squirrel then it visits the squirrel.
((("something" "needs" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If the dog is green then the dog sees the squirrel.
((("dog" "is" "green" "+")) -> ("dog" "sees" "squirrel" "+"))
Round, cold things are not young.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "-"))
If something is red then it does not need the dog.
((("something" "is" "red" "+")) -> ("something" "needs" "dog" "-"))
If something needs the squirrel then the squirrel sees the cow.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "sees" "cow" "+"))
The cow is round.
True
1
proof
[(triple1)]
("cow" "is" "round" "+")
triple1
The dog does not need the cow.
False
1
inv-proof
[(triple2)]
("dog" "needs" "cow" "-")
triple2
The squirrel sees the cow.
True
2
proof
[(((triple4) -> rule8))]
("squirrel" "sees" "cow" "+")
((triple4) -> (rule8 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel does not see the cow.
False
2
inv-proof
[(((triple4) -> rule8))]
("squirrel" "sees" "cow" "-")
((triple4) -> (rule8 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The tiger does not see the dog.
True
3
proof
[(((((triple4) -> rule4)) -> rule3))]
("tiger" "sees" "dog" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The tiger sees the dog.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule3))]
("tiger" "sees" "dog" "+")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2
The cow does not visit the dog.
Unknown
inv-rconc
[@1: The cow visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "dog" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The dog does not see the squirrel.
Unknown
inv-rconc
[@1: The dog sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "squirrel" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow does not need the tiger.
Unknown
inv-random
[@0: The cow needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "tiger" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cow is round.[(triple1)] The dog needs the cow.[(triple2)] The squirrel needs the tiger.[(triple3)] The tiger needs the squirrel.[(triple4)] @1: The squirrel sees the cow.[(((triple4) -> rule8))] The tiger visits the squirrel.[(((triple4) -> rule4))] @2: The tiger does not see the dog.[(((((triple4) -> rule4)) -> rule3))]
The cow is round.
("cow" "is" "round" "+")
triple1
The dog needs the cow.
("dog" "needs" "cow" "+")
triple2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple3
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple4
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
((triple4) -> (rule8 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((triple4) -> (rule4 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int2