The squirrel chases the tiger. The tiger eats the squirrel. The tiger is round. If the squirrel chases the tiger then the squirrel eats the tiger. If something is big and it chases the tiger then the tiger sees the squirrel. If something eats the tiger then it is red. If something chases the squirrel then the squirrel is red. If something is red then it does not see the tiger. If something eats the squirrel and the squirrel does not see the tiger then the squirrel is nice. If something sees the tiger and the tiger is not red then the tiger eats the squirrel. If the tiger chases the squirrel and the squirrel eats the tiger then the tiger eats the squirrel.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is round.
("tiger" "is" "round" "+")
If the squirrel chases the tiger then the squirrel eats the tiger.
((("squirrel" "chases" "tiger" "+")) -> ("squirrel" "eats" "tiger" "+"))
If something is big and it chases the tiger then the tiger sees the squirrel.
((("something" "is" "big" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "sees" "squirrel" "+"))
If something eats the tiger then it is red.
((("something" "eats" "tiger" "+")) -> ("something" "is" "red" "+"))
If something chases the squirrel then the squirrel is red.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If something is red then it does not see the tiger.
((("something" "is" "red" "+")) -> ("something" "sees" "tiger" "-"))
If something eats the squirrel and the squirrel does not see the tiger then the squirrel is nice.
((("something" "eats" "squirrel" "+") ("squirrel" "sees" "tiger" "~")) -> ("squirrel" "is" "nice" "+"))
If something sees the tiger and the tiger is not red then the tiger eats the squirrel.
((("something" "sees" "tiger" "+") ("tiger" "is" "red" "~")) -> ("tiger" "eats" "squirrel" "+"))
If the tiger chases the squirrel and the squirrel eats the tiger then the tiger eats the squirrel.
((("tiger" "chases" "squirrel" "+") ("squirrel" "eats" "tiger" "+")) -> ("tiger" "eats" "squirrel" "+"))
The squirrel chases the tiger.
True
1
proof
[(triple1)]
("squirrel" "chases" "tiger" "+")
triple1
The tiger does not eat the squirrel.
False
1
inv-proof
[(triple2)]
("tiger" "eats" "squirrel" "-")
triple2
The squirrel eats the tiger.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "eats" "tiger" "+")
((triple1) -> (rule1 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel does not eat the tiger.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "eats" "tiger" "-")
((triple1) -> (rule1 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("squirrel" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("squirrel" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel does not see the tiger.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule5))]
("squirrel" "sees" "tiger" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel sees the tiger.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule5))]
("squirrel" "sees" "tiger" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "red" "-")
The tiger sees the squirrel.
Unknown
rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "squirrel" "+")
The tiger does not chase the squirrel.
Unknown
inv-random
[@0: The tiger chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "squirrel" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The squirrel chases the tiger.[(triple1)] The tiger eats the squirrel.[(triple2)] The tiger is round.[(triple3)] @1: The squirrel eats the tiger.[(((triple1) -> rule1))] @2: The squirrel is red.[(((((triple1) -> rule1)) -> rule3))] @3: The squirrel does not see the tiger.[(((((((triple1) -> rule1)) -> rule3)) -> rule5))] @4: The squirrel is nice.[(((triple2 ((((((triple1) -> rule1)) -> rule3)) -> rule5)) -> rule6))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
((triple1) -> (rule1 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple2 ((((((triple1) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int4