The dog eats the tiger. The dog is green. The dog is not red. The squirrel does not eat the tiger. The squirrel visits the dog. The tiger eats the dog. The tiger eats the squirrel. If something is red then it is not round. If something visits the dog then it visits the squirrel. If the dog visits the tiger and the tiger is young then the dog eats the squirrel. If something chases the tiger and it does not eat the tiger then the tiger is green. If something visits the squirrel then the squirrel chases the tiger. If something visits the tiger then it chases the dog. If something chases the dog and the dog does not eat the squirrel then the squirrel does not visit the tiger. If the squirrel eats the dog and the squirrel does not chase the tiger then the dog is round.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is not red.
("dog" "is" "red" "-")
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
If something is red then it is not round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "-"))
If something visits the dog then it visits the squirrel.
((("something" "visits" "dog" "+")) -> ("something" "visits" "squirrel" "+"))
If the dog visits the tiger and the tiger is young then the dog eats the squirrel.
((("dog" "visits" "tiger" "+") ("tiger" "is" "young" "+")) -> ("dog" "eats" "squirrel" "+"))
If something chases the tiger and it does not eat the tiger then the tiger is green.
((("something" "chases" "tiger" "+") ("something" "eats" "tiger" "~")) -> ("tiger" "is" "green" "+"))
If something visits the squirrel then the squirrel chases the tiger.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "+"))
If something visits the tiger then it chases the dog.
((("something" "visits" "tiger" "+")) -> ("something" "chases" "dog" "+"))
If something chases the dog and the dog does not eat the squirrel then the squirrel does not visit the tiger.
((("something" "chases" "dog" "+") ("dog" "eats" "squirrel" "~")) -> ("squirrel" "visits" "tiger" "-"))
If the squirrel eats the dog and the squirrel does not chase the tiger then the dog is round.
((("squirrel" "eats" "dog" "+") ("squirrel" "chases" "tiger" "~")) -> ("dog" "is" "round" "+"))
The dog is not red.
True
1
proof
[(triple3)]
("dog" "is" "red" "-")
triple3
The tiger does not eat the squirrel.
False
1
inv-proof
[(triple7)]
("tiger" "eats" "squirrel" "-")
triple7
The squirrel visits the squirrel.
True
2
proof
[(((triple5) -> rule2))]
("squirrel" "visits" "squirrel" "+")
((triple5) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
False
2
inv-proof
[(((triple5) -> rule2))]
("squirrel" "visits" "squirrel" "-")
((triple5) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel chases the tiger.
True
3
proof
[(((((triple5) -> rule2)) -> rule5))]
("squirrel" "chases" "tiger" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel does not chase the tiger.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule5))]
("squirrel" "chases" "tiger" "-")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The tiger is green.
True
5
proof
[(((((((triple5) -> rule2)) -> rule5) triple4) -> rule4))]
("tiger" "is" "green" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The tiger is not green.
False
5
inv-proof
[(((((((triple5) -> rule2)) -> rule5) triple4) -> rule4))]
("tiger" "is" "green" "-")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The dog does not visit the squirrel.
Unknown
inv-rconc
[@1: The dog visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "squirrel" "-")
The squirrel chases the dog.
Unknown
rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "chases" "dog" "+")
The tiger does not chase the dog.
Unknown
inv-rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "dog" "-")
The tiger visits the squirrel.
Unknown
rconc
[@1: The tiger visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "squirrel" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The dog visits the tiger.
Unknown
random
[@0: The dog visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "tiger" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The squirrel visits the tiger.
Unknown
random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "+")
@0: The dog eats the tiger.[(triple1)] The dog is green.[(triple2)] The dog is not red.[(triple3)] The squirrel does not eat the tiger.[(triple4)] The squirrel visits the dog.[(triple5)] The tiger eats the dog.[(triple6)] The tiger eats the squirrel.[(triple7)] @1: The squirrel visits the squirrel.[(((triple5) -> rule2))] @2: The squirrel chases the tiger.[(((((triple5) -> rule2)) -> rule5))] @3: The tiger is green.[(((((((triple5) -> rule2)) -> rule5) triple4) -> rule4))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is not red.
("dog" "is" "red" "-")
triple3
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
triple4
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple5
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple6
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple7
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple5) -> (rule2 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2)) triple4) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3