The squirrel is big. The tiger chases the squirrel. If something needs the tiger and the tiger eats the squirrel then it needs the squirrel. If something needs the tiger and the tiger chases the squirrel then the tiger eats the squirrel. If something is big then it needs the tiger.
The squirrel is big.
("squirrel" "is" "big" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
If something needs the tiger and the tiger eats the squirrel then it needs the squirrel.
((("something" "needs" "tiger" "+") ("tiger" "eats" "squirrel" "+")) -> ("something" "needs" "squirrel" "+"))
If something needs the tiger and the tiger chases the squirrel then the tiger eats the squirrel.
((("something" "needs" "tiger" "+") ("tiger" "chases" "squirrel" "+")) -> ("tiger" "eats" "squirrel" "+"))
If something is big then it needs the tiger.
((("something" "is" "big" "+")) -> ("something" "needs" "tiger" "+"))
The squirrel is big.
True
1
proof
[(triple1)]
("squirrel" "is" "big" "+")
triple1
The tiger does not chase the squirrel.
False
1
inv-proof
[(triple2)]
("tiger" "chases" "squirrel" "-")
triple2
The squirrel needs the tiger.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "needs" "tiger" "+")
((triple1) -> (rule3 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "needs" "tiger" "-")
((triple1) -> (rule3 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The tiger eats the squirrel.
True
4
proof
[(((((triple1) -> rule3) triple2) -> rule2))]
("tiger" "eats" "squirrel" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int2
The tiger does not eat the squirrel.
False
4
inv-proof
[(((((triple1) -> rule3) triple2) -> rule2))]
("tiger" "eats" "squirrel" "-")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int2
The squirrel needs the squirrel.
True
7
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3) triple2) -> rule2)) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int3
The squirrel does not need the squirrel.
False
7
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3) triple2) -> rule2)) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int3
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger needs the squirrel.
Unknown
rconc
[@2: The tiger needs the squirrel.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("tiger" "needs" "squirrel" "+")
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 tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The squirrel does not eat the tiger.
Unknown
inv-random
[@0: The squirrel eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "tiger" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The squirrel is big.[(triple1)] The tiger chases the squirrel.[(triple2)] @1: The squirrel needs the tiger.[(((triple1) -> rule3))] @2: The tiger eats the squirrel.[(((((triple1) -> rule3) triple2) -> rule2))] @3: The squirrel needs the squirrel.[(((((triple1) -> rule3) ((((triple1) -> rule3) triple2) -> rule2)) -> rule1))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
((triple1) -> (rule3 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int3