The bear visits the tiger. The cat eats the bear. The cat is green. The cat is red. The cat likes the bear. The tiger is cold. The tiger is red. If something eats the bear then it visits the cat. If the tiger eats the bear then the bear eats the tiger. If the bear is green then the bear likes the cat. If something eats the bear and it is green then it eats the cat. If the bear is cold then the bear is kind. If something eats the cat then it visits the bear.
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something eats the bear then it visits the cat.
((("something" "eats" "bear" "+")) -> ("something" "visits" "cat" "+"))
If the tiger eats the bear then the bear eats the tiger.
((("tiger" "eats" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
If the bear is green then the bear likes the cat.
((("bear" "is" "green" "+")) -> ("bear" "likes" "cat" "+"))
If something eats the bear and it is green then it eats the cat.
((("something" "eats" "bear" "+") ("something" "is" "green" "+")) -> ("something" "eats" "cat" "+"))
If the bear is cold then the bear is kind.
((("bear" "is" "cold" "+")) -> ("bear" "is" "kind" "+"))
If something eats the cat then it visits the bear.
((("something" "eats" "cat" "+")) -> ("something" "visits" "bear" "+"))
The cat is red.
True
1
proof
[(triple4)]
("cat" "is" "red" "+")
triple4
The cat is not green.
False
1
inv-proof
[(triple3)]
("cat" "is" "green" "-")
triple3
The cat eats the cat.
True
3
proof
[(((triple2 triple3) -> rule4))]
("cat" "eats" "cat" "+")
((triple2 triple3) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "visits" "cat" "-")
((triple2) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the bear.
True
4
proof
[(((((triple2 triple3) -> rule4)) -> rule6))]
("cat" "visits" "bear" "+")
((((triple2 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat does not visit the bear.
False
4
inv-proof
[(((((triple2 triple3) -> rule4)) -> rule6))]
("cat" "visits" "bear" "-")
((((triple2 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The bear does not like the cat.
Unknown
inv-rconc
[@1: The bear likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "likes" "cat" "-")
The tiger visits the cat.
Unknown
rconc
[@1: The tiger visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "cat" "+")
The tiger does not visit the bear.
Unknown
inv-rconc
[@2: The tiger visits the bear.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("tiger" "visits" "bear" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The bear visits the tiger.[(triple1)] The cat eats the bear.[(triple2)] The cat is green.[(triple3)] The cat is red.[(triple4)] The cat likes the bear.[(triple5)] The tiger is cold.[(triple6)] The tiger is red.[(triple7)] @1: The cat eats the cat.[(((triple2 triple3) -> rule4))] The cat visits the cat.[(((triple2) -> rule1))] @2: The cat visits the bear.[(((((triple2 triple3) -> rule4)) -> rule6))]
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat likes the bear.
("cat" "likes" "bear" "+")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is red.
("tiger" "is" "red" "+")
triple7
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple2 triple3) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple2) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
((((triple2 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2