The cat is big. The cat is blue. The cat needs the cow. The cat visits the cow. The cow is blue. The cow needs the tiger. The cow sees the tiger. The tiger is red. The tiger is rough. The tiger needs the cat. The tiger needs the cow. The tiger sees the cat. The tiger sees the cow. The tiger visits the cat. The tiger visits the cow. If something needs the tiger then it visits the cat. If something is blue and it visits the cat then it is red. If something is red then it sees the cat. If something visits the cat and the cat visits the tiger then the cat visits the cow. If something sees the tiger then the tiger sees the cow. If something is red then it needs the cow.
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something needs the tiger then it visits the cat.
((("something" "needs" "tiger" "+")) -> ("something" "visits" "cat" "+"))
If something is blue and it visits the cat then it is red.
((("something" "is" "blue" "+") ("something" "visits" "cat" "+")) -> ("something" "is" "red" "+"))
If something is red then it sees the cat.
((("something" "is" "red" "+")) -> ("something" "sees" "cat" "+"))
If something visits the cat and the cat visits the tiger then the cat visits the cow.
((("something" "visits" "cat" "+") ("cat" "visits" "tiger" "+")) -> ("cat" "visits" "cow" "+"))
If something sees the tiger then the tiger sees the cow.
((("something" "sees" "tiger" "+")) -> ("tiger" "sees" "cow" "+"))
If something is red then it needs the cow.
((("something" "is" "red" "+")) -> ("something" "needs" "cow" "+"))
The tiger sees the cat.
True
1
proof
[(triple12 OR ((triple8) -> rule3))]
("tiger" "sees" "cat" "+")
triple12
((triple8) -> (rule3 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger does not see the cat.
False
1
inv-proof
[(triple12 OR ((triple8) -> rule3))]
("tiger" "sees" "cat" "-")
triple12
((triple8) -> (rule3 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The cow visits the cat.
True
2
proof
[(((triple6) -> rule1))]
("cow" "visits" "cat" "+")
((triple6) -> (rule1 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow does not visit the cat.
False
2
inv-proof
[(((triple6) -> rule1))]
("cow" "visits" "cat" "-")
((triple6) -> (rule1 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow is red.
True
4
proof
[(((triple5 ((triple6) -> rule1)) -> rule2))]
("cow" "is" "red" "+")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cow is not red.
False
4
inv-proof
[(((triple5 ((triple6) -> rule1)) -> rule2))]
("cow" "is" "red" "-")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cow sees the cat.
True
5
proof
[(((((triple5 ((triple6) -> rule1)) -> rule2)) -> rule3))]
("cow" "sees" "cat" "+")
((((triple5 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3
The cow does not see the cat.
False
5
inv-proof
[(((((triple5 ((triple6) -> rule1)) -> rule2)) -> rule3))]
("cow" "sees" "cat" "-")
((((triple5 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3
The cat does not see the cat.
Unknown
inv-rconc
[@3: The cat sees the cat.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat is not red.
Unknown
inv-rconc
[@2: The cat is red.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "is" "red" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cat does not see the cow.
Unknown
inv-random
[@0: The cat sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cow" "-")
The cat visits the tiger.
Unknown
random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "+")
@0: The cat is big.[(triple1)] The cat is blue.[(triple2)] The cat needs the cow.[(triple3)] The cat visits the cow.[(triple4)] The cow is blue.[(triple5)] The cow needs the tiger.[(triple6)] The cow sees the tiger.[(triple7)] The tiger is red.[(triple8)] The tiger is rough.[(triple9)] The tiger needs the cat.[(triple10)] The tiger needs the cow.[(triple11 OR ((triple8) -> rule6))] The tiger sees the cat.[(triple12 OR ((triple8) -> rule3))] The tiger sees the cow.[(triple13 OR ((triple7) -> rule5))] The tiger visits the cat.[(triple14)] The tiger visits the cow.[(triple15)] @1: The cow visits the cat.[(((triple6) -> rule1))] @2: The cow is red.[(((triple5 ((triple6) -> rule1)) -> rule2))] @3: The cow needs the cow.[(((((triple5 ((triple6) -> rule1)) -> rule2)) -> rule6))] The cow sees the cat.[(((((triple5 ((triple6) -> rule1)) -> rule2)) -> rule3))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
The cat visits the cow.
("cat" "visits" "cow" "+")
triple4
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple6
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple10
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple11
((triple8) -> (rule6 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple12
((triple8) -> (rule3 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple13
((triple7) -> (rule5 % int1))
The tiger sees the cow.
("tiger" "sees" "cow" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple14
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple15
The cow visits the cat.
("cow" "visits" "cat" "+")
((triple6) -> (rule1 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((triple5 ((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((triple5 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3
The cow sees the cat.
("cow" "sees" "cat" "+")
((((triple5 ((triple6) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3