The rabbit needs the tiger. The squirrel eats the rabbit. The squirrel is not green. The squirrel needs the rabbit. The tiger eats the rabbit. The tiger does not need the squirrel. The tiger visits the rabbit. If the squirrel visits the rabbit then the squirrel does not need the tiger. If something eats the squirrel and it does not visit the tiger then it does not need the squirrel. If something needs the rabbit then it visits the rabbit.
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is not green.
("squirrel" "is" "green" "-")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the squirrel visits the rabbit then the squirrel does not need the tiger.
((("squirrel" "visits" "rabbit" "+")) -> ("squirrel" "needs" "tiger" "-"))
If something eats the squirrel and it does not visit the tiger then it does not need the squirrel.
((("something" "eats" "squirrel" "+") ("something" "visits" "tiger" "~")) -> ("something" "needs" "squirrel" "-"))
If something needs the rabbit then it visits the rabbit.
((("something" "needs" "rabbit" "+")) -> ("something" "visits" "rabbit" "+"))
The tiger visits the rabbit.
True
1
proof
[(triple7)]
("tiger" "visits" "rabbit" "+")
triple7
The tiger does not eat the rabbit.
False
1
inv-proof
[(triple5)]
("tiger" "eats" "rabbit" "-")
triple5
The squirrel visits the rabbit.
True
2
proof
[(((triple4) -> rule3))]
("squirrel" "visits" "rabbit" "+")
((triple4) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel does not visit the rabbit.
False
2
inv-proof
[(((triple4) -> rule3))]
("squirrel" "visits" "rabbit" "-")
((triple4) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel does not need the tiger.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("squirrel" "needs" "tiger" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The squirrel needs the tiger.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("squirrel" "needs" "tiger" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "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 rabbit needs the tiger.[(triple1)] The squirrel eats the rabbit.[(triple2)] The squirrel is not green.[(triple3)] The squirrel needs the rabbit.[(triple4)] The tiger does not need the squirrel.[(triple6)] The tiger eats the rabbit.[(triple5)] The tiger visits the rabbit.[(triple7)] @1: The squirrel visits the rabbit.[(((triple4) -> rule3))] @2: The squirrel does not need the tiger.[(((((triple4) -> rule3)) -> rule1))]
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple2
The squirrel is not green.
("squirrel" "is" "green" "-")
triple3
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple4
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple6
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple5
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple7
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
((triple4) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel does not need the tiger.
("squirrel" "needs" "tiger" "-")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2