The cat does not eat the tiger. The squirrel visits the tiger. The tiger needs the squirrel. If something is nice then it visits the squirrel. If something needs the squirrel and it is not blue then it is not kind. If the tiger needs the squirrel then the tiger visits the cat. If something needs the tiger then the tiger does not eat the cat. If something eats the cat then it does not need the tiger. If something is cold and round then it visits the cat. If something needs the cat then it is nice. If something visits the cat then it eats the cat.
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If something is nice then it visits the squirrel.
((("something" "is" "nice" "+")) -> ("something" "visits" "squirrel" "+"))
If something needs the squirrel and it is not blue then it is not kind.
((("something" "needs" "squirrel" "+") ("something" "is" "blue" "~")) -> ("something" "is" "kind" "-"))
If the tiger needs the squirrel then the tiger visits the cat.
((("tiger" "needs" "squirrel" "+")) -> ("tiger" "visits" "cat" "+"))
If something needs the tiger then the tiger does not eat the cat.
((("something" "needs" "tiger" "+")) -> ("tiger" "eats" "cat" "-"))
If something eats the cat then it does not need the tiger.
((("something" "eats" "cat" "+")) -> ("something" "needs" "tiger" "-"))
If something is cold and round then it visits the cat.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "visits" "cat" "+"))
If something needs the cat then it is nice.
((("something" "needs" "cat" "+")) -> ("something" "is" "nice" "+"))
If something visits the cat then it eats the cat.
((("something" "visits" "cat" "+")) -> ("something" "eats" "cat" "+"))
The tiger needs the squirrel.
True
1
proof
[(triple3)]
("tiger" "needs" "squirrel" "+")
triple3
The tiger does not need the squirrel.
False
1
inv-proof
[(triple3)]
("tiger" "needs" "squirrel" "-")
triple3
The tiger visits the cat.
True
2
proof
[(((triple3) -> rule3))]
("tiger" "visits" "cat" "+")
((triple3) -> (rule3 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger does not visit the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("tiger" "visits" "cat" "-")
((triple3) -> (rule3 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger eats the cat.
True
3
proof
[(((((triple3) -> rule3)) -> rule8))]
("tiger" "eats" "cat" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger does not eat the cat.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule8))]
("tiger" "eats" "cat" "-")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger does not need the tiger.
True
4
proof
[(((((((triple3) -> rule3)) -> rule8)) -> rule5))]
("tiger" "needs" "tiger" "-")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
The tiger needs the tiger.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule8)) -> rule5))]
("tiger" "needs" "tiger" "+")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3
The tiger does not visit the squirrel.
Unknown
inv-rconc
[@2: The tiger visits the squirrel.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("tiger" "visits" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@2: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "visits" "cat" "-")
The squirrel is nice.
Unknown
rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "nice" "+")
The tiger does not need the cat.
Unknown
inv-random
[@0: The tiger needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cat" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The cat does not eat the squirrel.
Unknown
inv-random
[@0: The cat eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "squirrel" "-")
The squirrel eats the tiger.
Unknown
random
[@0: The squirrel eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "tiger" "+")
@0: The cat does not eat the tiger.[(triple1)] The squirrel visits the tiger.[(triple2)] The tiger needs the squirrel.[(triple3)] @1: The tiger visits the cat.[(((triple3) -> rule3))] @2: The tiger eats the cat.[(((((triple3) -> rule3)) -> rule8))] @3: The tiger does not need the tiger.[(((((((triple3) -> rule3)) -> rule8)) -> rule5))]
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
triple1
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple2
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple3
The tiger visits the cat.
("tiger" "visits" "cat" "+")
((triple3) -> (rule3 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int2
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int3