The cat chases the cow. The cat is cold. The cat is red. The cat is rough. The cat needs the cow. The cat sees the cow. The cow chases the cat. The cow is kind. The cow is rough. The cow is young. The cow needs the cat. The cow sees the cat. If someone needs the cow and the cow needs the cat then the cow chases the cat. If the cat sees the cow then the cat is red. If someone needs the cat then they see the cat. If someone sees the cow then they are young. If the cat chases the cow and the cat is rough then the cow needs the cat. If someone needs the cat then they need the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If someone needs the cow and the cow needs the cat then the cow chases the cat.
((("someone" "needs" "cow" "+") ("cow" "needs" "cat" "+")) -> ("cow" "chases" "cat" "+"))
If the cat sees the cow then the cat is red.
((("cat" "sees" "cow" "+")) -> ("cat" "is" "red" "+"))
If someone needs the cat then they see the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cow then they are young.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "young" "+"))
If the cat chases the cow and the cat is rough then the cow needs the cat.
((("cat" "chases" "cow" "+") ("cat" "is" "rough" "+")) -> ("cow" "needs" "cat" "+"))
If someone needs the cat then they need the cow.
((("someone" "needs" "cat" "+")) -> ("someone" "needs" "cow" "+"))
The cow chases the cat.
True
1
proof
[(triple7 OR ((triple5 triple11) -> rule1) OR ((triple5 ((triple1 triple4) -> rule5)) -> rule1) OR ((((triple11) -> rule6) triple11) -> rule1) OR ((((triple11) -> rule6) ((triple1 triple4) -> rule5)) -> rule1) OR ((((((triple1 triple4) -> rule5)) -> rule6) triple11) -> rule1) OR ((((((triple1 triple4) -> rule5)) -> rule6) ((triple1 triple4) -> rule5)) -> rule1))]
("cow" "chases" "cat" "+")
triple7
((triple5 triple11) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
((triple5 ((triple1 triple4) -> (rule5 % int2))) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
((((triple11) -> (rule6 % int2)) triple11) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
((((triple11) -> (rule6 % int3)) ((triple1 triple4) -> (rule5 % int2))) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
((((((triple1 triple4) -> (rule5 % int3))) -> (rule6 % int2)) triple11) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
int3
((((((triple1 triple4) -> (rule5 % int3))) -> (rule6 % int2)) ((triple1 triple4) -> (rule5 % int3))) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
int3
The cat is not rough.
False
1
inv-proof
[(triple4)]
("cat" "is" "rough" "-")
triple4
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat chases the cow.[(triple1)] The cat is cold.[(triple2)] The cat is red.[(triple3 OR ((triple6) -> rule2))] The cat is rough.[(triple4)] The cat needs the cow.[(triple5)] The cat sees the cow.[(triple6)] The cow chases the cat.[(triple7 OR ((triple5 triple11) -> rule1) OR ((triple5 ((triple1 triple4) -> rule5)) -> rule1) OR ((((triple11) -> rule6) triple11) -> rule1) OR ((((triple11) -> rule6) ((triple1 triple4) -> rule5)) -> rule1) OR ((((((triple1 triple4) -> rule5)) -> rule6) triple11) -> rule1) OR ((((((triple1 triple4) -> rule5)) -> rule6) ((triple1 triple4) -> rule5)) -> rule1))] The cow is kind.[(triple8)] The cow is rough.[(triple9)] The cow is young.[(triple10)] The cow needs the cat.[(triple11 OR ((triple1 triple4) -> rule5))] The cow sees the cat.[(triple12 OR ((triple11) -> rule3) OR ((((triple1 triple4) -> rule5)) -> rule3))] @1: The cat is young.[(((triple6) -> rule4))] The cow needs the cow.[(((triple11) -> rule6) OR ((((triple1 triple4) -> rule5)) -> rule6))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
((triple6) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat needs the cow.
("cat" "needs" "cow" "+")
triple5
The cat sees the cow.
("cat" "sees" "cow" "+")
triple6
The cow chases the cat.
("cow" "chases" "cat" "+")
triple7
((triple5 triple11) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
((triple5 ((triple1 triple4) -> (rule5 % int2))) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
((((triple11) -> (rule6 % int2)) triple11) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
((((triple11) -> (rule6 % int3)) ((triple1 triple4) -> (rule5 % int2))) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
((((((triple1 triple4) -> (rule5 % int3))) -> (rule6 % int2)) triple11) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
int3
((((((triple1 triple4) -> (rule5 % int3))) -> (rule6 % int2)) ((triple1 triple4) -> (rule5 % int3))) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow needs the cat.
("cow" "needs" "cat" "+")
int3
The cow is kind.
("cow" "is" "kind" "+")
triple8
The cow is rough.
("cow" "is" "rough" "+")
triple9
The cow is young.
("cow" "is" "young" "+")
triple10
The cow needs the cat.
("cow" "needs" "cat" "+")
triple11
((triple1 triple4) -> (rule5 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
triple12
((triple11) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
((((triple1 triple4) -> (rule5 % int2))) -> (rule3 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
((triple6) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple11) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
((((triple1 triple4) -> (rule5 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow needs the cat.
("cow" "needs" "cat" "+")
int2