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