The cat eats the cow. The cat eats the tiger. The cat is big. The cat visits the tiger. The cow is blue. The cow likes the cat. The cow visits the tiger. The tiger eats the cow. The tiger is blue. The tiger is cold. The tiger is red. The tiger likes the cow. If someone likes the tiger then they like the cat. If someone is cold then they do not visit the cow. If someone is red and blue then they eat the cat. If the tiger eats the cat then the cat visits the cow. If the cow visits the tiger and the cat does not like the cow then the cow is big. If someone visits the cow and the cow is red then the cow is big.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If someone likes the tiger then they like the cat.
((("someone" "likes" "tiger" "+")) -> ("someone" "likes" "cat" "+"))
If someone is cold then they do not visit the cow.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "cow" "-"))
If someone is red and blue then they eat the cat.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "eats" "cat" "+"))
If the tiger eats the cat then the cat visits the cow.
((("tiger" "eats" "cat" "+")) -> ("cat" "visits" "cow" "+"))
If the cow visits the tiger and the cat does not like the cow then the cow is big.
((("cow" "visits" "tiger" "+") ("cat" "likes" "cow" "~")) -> ("cow" "is" "big" "+"))
If someone visits the cow and the cow is red then the cow is big.
((("someone" "visits" "cow" "+") ("cow" "is" "red" "+")) -> ("cow" "is" "big" "+"))
The cow visits the tiger.
True
1
proof
[(triple7)]
("cow" "visits" "tiger" "+")
triple7
The tiger does not like the cow.
False
1
inv-proof
[(triple12)]
("tiger" "likes" "cow" "-")
triple12
The tiger eats the cat.
True
3
proof
[(((triple11 triple9) -> rule3))]
("tiger" "eats" "cat" "+")
((triple11 triple9) -> (rule3 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger does not eat the cat.
False
3
inv-proof
[(((triple11 triple9) -> rule3))]
("tiger" "eats" "cat" "-")
((triple11 triple9) -> (rule3 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The cat visits the cow.
True
4
proof
[(((((triple11 triple9) -> rule3)) -> rule4))]
("cat" "visits" "cow" "+")
((((triple11 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2
The cat does not visit the cow.
False
4
inv-proof
[(((((triple11 triple9) -> rule3)) -> rule4))]
("cat" "visits" "cow" "-")
((((triple11 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "big" "-")
The tiger likes the cat.
Unknown
rconc
[@1: The tiger likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "cat" "+")
The cow does not eat the cat.
Unknown
inv-rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "cat" "-")
The cow eats the tiger.
Unknown
random
[@0: The cow eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "tiger" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The cow likes the tiger.
Unknown
random
[@0: The cow likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "tiger" "+")
@0: The cat eats the cow.[(triple1)] The cat eats the tiger.[(triple2)] The cat is big.[(triple3)] The cat visits the tiger.[(triple4)] The cow is blue.[(triple5)] The cow likes the cat.[(triple6)] The cow visits the tiger.[(triple7)] The tiger eats the cow.[(triple8)] The tiger is blue.[(triple9)] The tiger is cold.[(triple10)] The tiger is red.[(triple11)] The tiger likes the cow.[(triple12)] @1: The tiger does not visit the cow.[(((triple10) -> rule2))] The tiger eats the cat.[(((triple11 triple9) -> rule3))] @2: The cat visits the cow.[(((((triple11 triple9) -> rule3)) -> rule4))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple4
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow likes the cat.
("cow" "likes" "cat" "+")
triple6
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple7
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple12
The tiger does not visit the cow.
("tiger" "visits" "cow" "-")
((triple10) -> (rule2 % int1))
The tiger does not visit the cow.
("tiger" "visits" "cow" "-")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((triple11 triple9) -> (rule3 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
((((triple11 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2