The cat chases the tiger. The cat does not eat the tiger. The cat needs the tiger. The tiger chases the cat. The tiger eats the cat. The tiger is blue. The tiger is green. The tiger is rough. The tiger is not young. The tiger needs the cat. If something needs the tiger then it needs the cat. If something needs the tiger then it needs the cat. If something is young then it needs the tiger. If the cat is young then the cat chases the tiger. If something needs the cat then it chases the cat. If something eats the cat and the cat eats the tiger then the cat is not green.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If something needs the tiger then it needs the cat.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "cat" "+"))
If something needs the tiger then it needs the cat.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "cat" "+"))
If something is young then it needs the tiger.
((("something" "is" "young" "+")) -> ("something" "needs" "tiger" "+"))
If the cat is young then the cat chases the tiger.
((("cat" "is" "young" "+")) -> ("cat" "chases" "tiger" "+"))
If something needs the cat then it chases the cat.
((("something" "needs" "cat" "+")) -> ("something" "chases" "cat" "+"))
If something eats the cat and the cat eats the tiger then the cat is not green.
((("something" "eats" "cat" "+") ("cat" "eats" "tiger" "+")) -> ("cat" "is" "green" "-"))
The cat needs the tiger.
True
1
proof
[(triple3)]
("cat" "needs" "tiger" "+")
triple3
The tiger does not eat the cat.
False
1
inv-proof
[(triple5)]
("tiger" "eats" "cat" "-")
triple5
The cat needs the cat.
True
2
proof
[(((triple3) -> rule1) OR ((triple3) -> rule2))]
("cat" "needs" "cat" "+")
((triple3) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
((triple3) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple3) -> rule2))]
("cat" "needs" "cat" "-")
((triple3) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
((triple3) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The cat does not eat the tiger.[(triple2)] The cat needs the tiger.[(triple3)] The tiger chases the cat.[(triple4 OR ((triple10) -> rule5))] The tiger eats the cat.[(triple5)] The tiger is blue.[(triple6)] The tiger is green.[(triple7)] The tiger is not young.[(triple9)] The tiger is rough.[(triple8)] The tiger needs the cat.[(triple10)] @1: The cat needs the cat.[(((triple3) -> rule1) OR ((triple3) -> rule2))] @2: The cat chases the cat.[(((((triple3) -> rule1)) -> rule5) OR ((((triple3) -> rule2)) -> rule5))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple4
((triple10) -> (rule5 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger is not young.
("tiger" "is" "young" "-")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple8
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple10
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple3) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
((triple3) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2