The cat is cold. The cat is kind. The cat does not visit the squirrel. The cat visits the tiger. The rabbit chases the tiger. The rabbit eats the squirrel. The rabbit visits the tiger. The squirrel does not chase the rabbit. The squirrel chases the tiger. The squirrel visits the rabbit. The tiger is red. The tiger is rough. If something chases the squirrel then the squirrel does not eat the tiger. If something chases the cat and it is cold then the cat chases the squirrel. If something eats the rabbit and it does not visit the rabbit then the rabbit eats the tiger. If the rabbit eats the squirrel then the rabbit visits the squirrel. If something eats the rabbit then it chases the tiger. Big things are not rough. If something eats the squirrel and it visits the squirrel then the squirrel is big. If the cat does not chase the squirrel and the squirrel does not visit the tiger then the tiger eats the squirrel.
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat does not visit the squirrel.
("cat" "visits" "squirrel" "-")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If something chases the squirrel then the squirrel does not eat the tiger.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "eats" "tiger" "-"))
If something chases the cat and it is cold then the cat chases the squirrel.
((("something" "chases" "cat" "+") ("something" "is" "cold" "+")) -> ("cat" "chases" "squirrel" "+"))
If something eats the rabbit and it does not visit the rabbit then the rabbit eats the tiger.
((("something" "eats" "rabbit" "+") ("something" "visits" "rabbit" "~")) -> ("rabbit" "eats" "tiger" "+"))
If the rabbit eats the squirrel then the rabbit visits the squirrel.
((("rabbit" "eats" "squirrel" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If something eats the rabbit then it chases the tiger.
((("something" "eats" "rabbit" "+")) -> ("something" "chases" "tiger" "+"))
Big things are not rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "-"))
If something eats the squirrel and it visits the squirrel then the squirrel is big.
((("something" "eats" "squirrel" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
If the cat does not chase the squirrel and the squirrel does not visit the tiger then the tiger eats the squirrel.
((("cat" "chases" "squirrel" "~") ("squirrel" "visits" "tiger" "~")) -> ("tiger" "eats" "squirrel" "+"))
The cat is kind.
True
1
proof
[(triple2)]
("cat" "is" "kind" "+")
triple2
The tiger is not red.
False
1
inv-proof
[(triple11)]
("tiger" "is" "red" "-")
triple11
The rabbit visits the squirrel.
True
2
proof
[(((triple6) -> rule4))]
("rabbit" "visits" "squirrel" "+")
((triple6) -> (rule4 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit does not visit the squirrel.
False
2
inv-proof
[(((triple6) -> rule4))]
("rabbit" "visits" "squirrel" "-")
((triple6) -> (rule4 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel is big.
True
4
proof
[(((triple6 ((triple6) -> rule4)) -> rule7))]
("squirrel" "is" "big" "+")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The squirrel is not big.
False
4
inv-proof
[(((triple6 ((triple6) -> rule4)) -> rule7))]
("squirrel" "is" "big" "-")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The squirrel is not rough.
True
5
proof
[(((((triple6 ((triple6) -> rule4)) -> rule7)) -> rule6))]
("squirrel" "is" "rough" "-")
((((triple6 ((triple6) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
The squirrel is rough.
False
5
inv-proof
[(((((triple6 ((triple6) -> rule4)) -> rule7)) -> rule6))]
("squirrel" "is" "rough" "+")
((((triple6 ((triple6) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
The cat does not chase the squirrel.
Unknown
inv-rconc
[@1: The cat chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "squirrel" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The cat does not chase the tiger.
Unknown
inv-rconc
[@1: The cat chases the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "chases" "tiger" "-")
The tiger eats the squirrel.
Unknown
rconc
[@1: The tiger eats the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "squirrel" "+")
The squirrel does not eat the rabbit.
Unknown
inv-random
[@0: The squirrel eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "rabbit" "-")
The cat eats the tiger.
Unknown
random
[@0: The cat eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "tiger" "+")
The squirrel does not eat the tiger.
Unknown
inv-random
[@0: The squirrel eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "tiger" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The cat does not visit the squirrel.[(triple3)] The cat is cold.[(triple1)] The cat is kind.[(triple2)] The cat visits the tiger.[(triple4)] The rabbit chases the tiger.[(triple5)] The rabbit eats the squirrel.[(triple6)] The rabbit visits the tiger.[(triple7)] The squirrel chases the tiger.[(triple9)] The squirrel does not chase the rabbit.[(triple8)] The squirrel visits the rabbit.[(triple10)] The tiger is red.[(triple11)] The tiger is rough.[(triple12)] @1: The rabbit visits the squirrel.[(((triple6) -> rule4))] @2: The squirrel is big.[(((triple6 ((triple6) -> rule4)) -> rule7))] @3: The squirrel is not rough.[(((((triple6 ((triple6) -> rule4)) -> rule7)) -> rule6))]
The cat does not visit the squirrel.
("cat" "visits" "squirrel" "-")
triple3
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple4
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple5
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple6
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple7
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple9
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
triple8
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((triple6) -> (rule4 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule7 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The squirrel is not rough.
("squirrel" "is" "rough" "-")
((((triple6 ((triple6) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not rough.
("squirrel" "is" "rough" "-")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3