The squirrel is nice. The tiger chases the squirrel. The tiger visits the squirrel. If someone chases the squirrel then the squirrel eats the tiger. If someone eats the squirrel then they are nice. If someone chases the tiger then the tiger is not nice. If someone eats the tiger then they eat the squirrel. If someone is green then they are round. If the tiger eats the squirrel then the tiger is round. If the squirrel is young and the tiger does not eat the squirrel then the squirrel is nice. If someone is nice and they eat the squirrel then the squirrel visits the tiger.
The squirrel is nice.
("squirrel" "is" "nice" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone chases the squirrel then the squirrel eats the tiger.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "eats" "tiger" "+"))
If someone eats the squirrel then they are nice.
((("someone" "eats" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
If someone chases the tiger then the tiger is not nice.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "nice" "-"))
If someone eats the tiger then they eat the squirrel.
((("someone" "eats" "tiger" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If the tiger eats the squirrel then the tiger is round.
((("tiger" "eats" "squirrel" "+")) -> ("tiger" "is" "round" "+"))
If the squirrel is young and the tiger does not eat the squirrel then the squirrel is nice.
((("squirrel" "is" "young" "+") ("tiger" "eats" "squirrel" "~")) -> ("squirrel" "is" "nice" "+"))
If someone is nice and they eat the squirrel then the squirrel visits the tiger.
((("someone" "is" "nice" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "visits" "tiger" "+"))
The tiger chases the squirrel.
True
1
proof
[(triple2)]
("tiger" "chases" "squirrel" "+")
triple2
The tiger does not visit the squirrel.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "squirrel" "-")
triple3
The squirrel eats the tiger.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "eats" "tiger" "+")
((triple2) -> (rule1 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel does not eat the tiger.
False
2
inv-proof
[(((triple2) -> rule1))]
("squirrel" "eats" "tiger" "-")
((triple2) -> (rule1 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel eats the squirrel.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("squirrel" "eats" "squirrel" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel does not eat the squirrel.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("squirrel" "eats" "squirrel" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel visits the tiger.
True
5
proof
[(((triple1 ((((triple2) -> rule1)) -> rule4)) -> rule8) OR ((((((((triple2) -> rule1)) -> rule4)) -> rule2) ((((triple2) -> rule1)) -> rule4)) -> rule8))]
("squirrel" "visits" "tiger" "+")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int4
The squirrel does not visit the tiger.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule1)) -> rule4)) -> rule8) OR ((((((((triple2) -> rule1)) -> rule4)) -> rule2) ((((triple2) -> rule1)) -> rule4)) -> rule8))]
("squirrel" "visits" "tiger" "-")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int4
The tiger is not round.
Unknown
inv-rconc
[@2: The tiger is round.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("tiger" "is" "round" "-")
The tiger eats the squirrel.
Unknown
rconc
[@1: The tiger eats the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "eats" "squirrel" "+")
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "round" "-")
The tiger is nice.
Unknown
rconc
[@2: The tiger is nice.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("tiger" "is" "nice" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
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 green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The squirrel is nice.[(triple1 OR ((((((triple2) -> rule1)) -> rule4)) -> rule2))] The tiger chases the squirrel.[(triple2)] The tiger visits the squirrel.[(triple3)] @1: The squirrel eats the tiger.[(((triple2) -> rule1))] @2: The squirrel eats the squirrel.[(((((triple2) -> rule1)) -> rule4))] @3: The squirrel visits the tiger.[(((triple1 ((((triple2) -> rule1)) -> rule4)) -> rule8) OR ((((((((triple2) -> rule1)) -> rule4)) -> rule2) ((((triple2) -> rule1)) -> rule4)) -> rule8))]
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple1
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
((triple2) -> (rule1 % int1))
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int2
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((((triple2) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule8 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
int4