The bear likes the cat. The cat likes the cow. The cow eats the tiger. The tiger is round. If something is young then it sees the bear. If something likes the cat then it is young. If something is cold then it sees the cow. If something eats the cat and the cat eats the cow then it likes the tiger. If something sees the cow and it sees the tiger then the tiger likes the cat. If something is blue and it sees the cow then the cow eats the bear.
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something is young then it sees the bear.
((("something" "is" "young" "+")) -> ("something" "sees" "bear" "+"))
If something likes the cat then it is young.
((("something" "likes" "cat" "+")) -> ("something" "is" "young" "+"))
If something is cold then it sees the cow.
((("something" "is" "cold" "+")) -> ("something" "sees" "cow" "+"))
If something eats the cat and the cat eats the cow then it likes the tiger.
((("something" "eats" "cat" "+") ("cat" "eats" "cow" "+")) -> ("something" "likes" "tiger" "+"))
If something sees the cow and it sees the tiger then the tiger likes the cat.
((("something" "sees" "cow" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If something is blue and it sees the cow then the cow eats the bear.
((("something" "is" "blue" "+") ("something" "sees" "cow" "+")) -> ("cow" "eats" "bear" "+"))
The cat likes the cow.
True
1
proof
[(triple2)]
("cat" "likes" "cow" "+")
triple2
The bear does not like the cat.
False
1
inv-proof
[(triple1)]
("bear" "likes" "cat" "-")
triple1
The bear is young.
True
2
proof
[(((triple1) -> rule2))]
("bear" "is" "young" "+")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "is" "young" "-")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the bear.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("bear" "sees" "bear" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear does not see the bear.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("bear" "sees" "bear" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The tiger does not like the cat.
Unknown
inv-rconc
[@1: The tiger likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "likes" "cat" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "cow" "+")
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger likes the cow.
Unknown
random
[@0: The tiger likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cow" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The bear likes the cat.[(triple1)] The cat likes the cow.[(triple2)] The cow eats the tiger.[(triple3)] The tiger is round.[(triple4)] @1: The bear is young.[(((triple1) -> rule2))] @2: The bear sees the bear.[(((((triple1) -> rule2)) -> rule1))]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple3
The tiger is round.
("tiger" "is" "round" "+")
triple4
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2