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