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