The rabbit chases the tiger. The rabbit is nice. The rabbit sees the squirrel. The squirrel chases the rabbit. The squirrel is red. The squirrel sees the rabbit. The squirrel sees the tiger. The tiger chases the squirrel. The tiger is big. The tiger is blue. If something sees the squirrel then it chases the squirrel. If something is green then it sees the squirrel. If the tiger visits the rabbit and the rabbit chases the squirrel then the squirrel is blue. All red things are nice. If something chases the squirrel then it visits the rabbit. If something chases the squirrel and the squirrel visits the tiger then the tiger visits the squirrel. If the tiger is big and the tiger visits the squirrel then the tiger visits the rabbit. If something chases the tiger then it sees the tiger.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something sees the squirrel then it chases the squirrel.
((("something" "sees" "squirrel" "+")) -> ("something" "chases" "squirrel" "+"))
If something is green then it sees the squirrel.
((("something" "is" "green" "+")) -> ("something" "sees" "squirrel" "+"))
If the tiger visits the rabbit and the rabbit chases the squirrel then the squirrel is blue.
((("tiger" "visits" "rabbit" "+") ("rabbit" "chases" "squirrel" "+")) -> ("squirrel" "is" "blue" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something chases the squirrel then it visits the rabbit.
((("something" "chases" "squirrel" "+")) -> ("something" "visits" "rabbit" "+"))
If something chases the squirrel and the squirrel visits the tiger then the tiger visits the squirrel.
((("something" "chases" "squirrel" "+") ("squirrel" "visits" "tiger" "+")) -> ("tiger" "visits" "squirrel" "+"))
If the tiger is big and the tiger visits the squirrel then the tiger visits the rabbit.
((("tiger" "is" "big" "+") ("tiger" "visits" "squirrel" "+")) -> ("tiger" "visits" "rabbit" "+"))
If something chases the tiger then it sees the tiger.
((("something" "chases" "tiger" "+")) -> ("something" "sees" "tiger" "+"))
The squirrel chases the rabbit.
True
1
proof
[(triple4)]
("squirrel" "chases" "rabbit" "+")
triple4
The squirrel does not see the tiger.
False
1
inv-proof
[(triple7)]
("squirrel" "sees" "tiger" "-")
triple7
The squirrel is nice.
True
2
proof
[(((triple5) -> rule4))]
("squirrel" "is" "nice" "+")
((triple5) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple5) -> rule4))]
("squirrel" "is" "nice" "-")
((triple5) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is blue.
True
5
proof
[(((((triple8) -> rule5) ((triple3) -> rule1)) -> rule3))]
("squirrel" "is" "blue" "+")
((((triple8) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
The rabbit does not visit the rabbit.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("rabbit" "visits" "rabbit" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The tiger does not see the squirrel.
Unknown
inv-rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "squirrel" "-")
The squirrel visits the rabbit.
Unknown
rconc
[@3: The squirrel visits the rabbit.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- FAIL)]]
("squirrel" "visits" "rabbit" "+")
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "nice" "-")
The tiger chases the rabbit.
Unknown
random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "+")
The squirrel does not visit the tiger.
Unknown
inv-random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The rabbit chases the tiger.[(triple1)] The rabbit is nice.[(triple2)] The rabbit sees the squirrel.[(triple3)] The squirrel chases the rabbit.[(triple4)] The squirrel is red.[(triple5)] The squirrel sees the rabbit.[(triple6)] The squirrel sees the tiger.[(triple7)] The tiger chases the squirrel.[(triple8)] The tiger is big.[(triple9)] The tiger is blue.[(triple10)] @1: The rabbit chases the squirrel.[(((triple3) -> rule1))] The rabbit sees the tiger.[(((triple1) -> rule8))] The squirrel is nice.[(((triple5) -> rule4))] The tiger visits the rabbit.[(((triple8) -> rule5))] @2: The rabbit visits the rabbit.[(((((triple3) -> rule1)) -> rule5))] The squirrel is blue.[(((((triple8) -> rule5) ((triple3) -> rule1)) -> rule3))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple3
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple4
The squirrel is red.
("squirrel" "is" "red" "+")
triple5
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple6
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
((triple3) -> (rule1 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((triple1) -> (rule8 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple5) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((triple8) -> (rule5 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple8) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3