The cat likes the cow. The cat sees the tiger. The cow is red. The tiger is rough. The tiger sees the cat. The tiger visits the cat. The tiger visits the cow. If something is cold and it visits the cow then it visits the tiger. If something visits the cat then it is rough. If something visits the cat then it likes the cat. If the tiger visits the cat and the cat likes the tiger then the cat likes the cow. If something likes the cow then the cow likes the tiger. If something sees the cat then the cat is young.
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cow is red.
("cow" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something is cold and it visits the cow then it visits the tiger.
((("something" "is" "cold" "+") ("something" "visits" "cow" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the cat then it is rough.
((("something" "visits" "cat" "+")) -> ("something" "is" "rough" "+"))
If something visits the cat then it likes the cat.
((("something" "visits" "cat" "+")) -> ("something" "likes" "cat" "+"))
If the tiger visits the cat and the cat likes the tiger then the cat likes the cow.
((("tiger" "visits" "cat" "+") ("cat" "likes" "tiger" "+")) -> ("cat" "likes" "cow" "+"))
If something likes the cow then the cow likes the tiger.
((("something" "likes" "cow" "+")) -> ("cow" "likes" "tiger" "+"))
If something sees the cat then the cat is young.
((("something" "sees" "cat" "+")) -> ("cat" "is" "young" "+"))
The cat sees the tiger.
True
1
proof
[(triple2)]
("cat" "sees" "tiger" "+")
triple2
The tiger does not see the cat.
False
1
inv-proof
[(triple5)]
("tiger" "sees" "cat" "-")
triple5
The tiger likes the cat.
True
2
proof
[(((triple6) -> rule3))]
("tiger" "likes" "cat" "+")
((triple6) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cow does not like the tiger.
False
2
inv-proof
[(((triple1) -> rule5))]
("cow" "likes" "tiger" "-")
((triple1) -> (rule5 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow does not like the cat.
Unknown
inv-rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "cat" "-")
The cow visits the tiger.
Unknown
rconc
[@1: The cow visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "tiger" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cat likes the cow.[(triple1)] The cat sees the tiger.[(triple2)] The cow is red.[(triple3)] The tiger is rough.[(triple4 OR ((triple6) -> rule2))] The tiger sees the cat.[(triple5)] The tiger visits the cat.[(triple6)] The tiger visits the cow.[(triple7)] @1: The cat is young.[(((triple5) -> rule6))] The cow likes the tiger.[(((triple1) -> rule5))] The tiger likes the cat.[(((triple6) -> rule3))]
The cat likes the cow.
("cat" "likes" "cow" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
((triple6) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple5
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7
The cat is young.
("cat" "is" "young" "+")
((triple5) -> (rule6 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple1) -> (rule5 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((triple6) -> (rule3 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1