The cat chases the cow. The cat is big. The cat is cold. The cat is green. The cat is red. The cat is rough. The cat needs the cow. The cat visits the cow. The cow chases the cat. The cow is big. The cow is cold. The cow is green. The cow is red. The cow is rough. The cow needs the cat. The cow visits the cat. If someone chases the cow and the cow visits the cat then they chase the cat. If someone is rough then they need the cow. If someone visits the cat and the cat chases the cow then the cow needs the cat. If someone is big and they chase the cat then they visit the cat. If the cow is rough and the cow chases the cat then the cat is green. If someone visits the cat and they are cold then they are green. If someone is cold then they visit the cow. If someone visits the cat then they need the cat.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If someone chases the cow and the cow visits the cat then they chase the cat.
((("someone" "chases" "cow" "+") ("cow" "visits" "cat" "+")) -> ("someone" "chases" "cat" "+"))
If someone is rough then they need the cow.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "cow" "+"))
If someone visits the cat and the cat chases the cow then the cow needs the cat.
((("someone" "visits" "cat" "+") ("cat" "chases" "cow" "+")) -> ("cow" "needs" "cat" "+"))
If someone is big and they chase the cat then they visit the cat.
((("someone" "is" "big" "+") ("someone" "chases" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If the cow is rough and the cow chases the cat then the cat is green.
((("cow" "is" "rough" "+") ("cow" "chases" "cat" "+")) -> ("cat" "is" "green" "+"))
If someone visits the cat and they are cold then they are green.
((("someone" "visits" "cat" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is cold then they visit the cow.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "cow" "+"))
If someone visits the cat then they need the cat.
((("someone" "visits" "cat" "+")) -> ("someone" "needs" "cat" "+"))
The cow is green.
True
1
proof
[(triple12 OR ((triple16 triple11) -> rule6) OR ((((triple10 triple9) -> rule4) triple11) -> rule6))]
("cow" "is" "green" "+")
triple12
((triple16 triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((triple10 triple9) -> (rule4 % int2)) triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat does not chase the cow.
False
1
inv-proof
[(triple1)]
("cat" "chases" "cow" "-")
triple1
The cow visits the cow.
True
2
proof
[(((triple11) -> rule7))]
("cow" "visits" "cow" "+")
((triple11) -> (rule7 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple11) -> rule7))]
("cow" "visits" "cow" "-")
((triple11) -> (rule7 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cat visits the cat.
True
5
proof
[(((triple2 ((triple1 triple16) -> rule1)) -> rule4) OR ((triple2 ((triple1 ((triple10 triple9) -> rule4)) -> rule1)) -> rule4))]
("cat" "visits" "cat" "+")
((triple2 ((triple1 triple16) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
((triple2 ((triple1 ((triple10 triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3
The cat does not visit the cat.
False
5
inv-proof
[(((triple2 ((triple1 triple16) -> rule1)) -> rule4) OR ((triple2 ((triple1 ((triple10 triple9) -> rule4)) -> rule1)) -> rule4))]
("cat" "visits" "cat" "-")
((triple2 ((triple1 triple16) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
((triple2 ((triple1 ((triple10 triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3
The cat needs the cat.
True
6
proof
[(((((triple2 ((triple1 triple16) -> rule1)) -> rule4)) -> rule8) OR ((((triple2 ((triple1 ((triple10 triple9) -> rule4)) -> rule1)) -> rule4)) -> rule8))]
("cat" "needs" "cat" "+")
((((triple2 ((triple1 triple16) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple2 ((triple1 ((triple10 triple9) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The cow visits the cat.
("cow" "visits" "cat" "+")
int4
The cat does not need the cat.
False
6
inv-proof
[(((((triple2 ((triple1 triple16) -> rule1)) -> rule4)) -> rule8) OR ((((triple2 ((triple1 ((triple10 triple9) -> rule4)) -> rule1)) -> rule4)) -> rule8))]
("cat" "needs" "cat" "-")
((((triple2 ((triple1 triple16) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple2 ((triple1 ((triple10 triple9) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The cow visits the cat.
("cow" "visits" "cat" "+")
int4
@0: The cat chases the cow.[(triple1)] The cat is big.[(triple2)] The cat is cold.[(triple3)] The cat is green.[(triple4 OR ((triple14 triple9) -> rule5) OR ((((triple2 ((triple1 triple16) -> rule1)) -> rule4) triple3) -> rule6) OR ((((triple2 ((triple1 ((triple10 triple9) -> rule4)) -> rule1)) -> rule4) triple3) -> rule6))] The cat is red.[(triple5)] The cat is rough.[(triple6)] The cat needs the cow.[(triple7 OR ((triple6) -> rule2))] The cat visits the cow.[(triple8 OR ((triple3) -> rule7))] The cow chases the cat.[(triple9)] The cow is big.[(triple10)] The cow is cold.[(triple11)] The cow is green.[(triple12 OR ((triple16 triple11) -> rule6) OR ((((triple10 triple9) -> rule4) triple11) -> rule6))] The cow is red.[(triple13)] The cow is rough.[(triple14)] The cow needs the cat.[(triple15 OR ((triple16) -> rule8) OR ((triple16 triple1) -> rule3) OR ((((triple10 triple9) -> rule4)) -> rule8) OR ((((triple10 triple9) -> rule4) triple1) -> rule3) OR ((((triple2 ((triple1 triple16) -> rule1)) -> rule4) triple1) -> rule3) OR ((((triple2 ((triple1 ((triple10 triple9) -> rule4)) -> rule1)) -> rule4) triple1) -> rule3))] The cow visits the cat.[(triple16 OR ((triple10 triple9) -> rule4))] @1: The cat chases the cat.[(((triple1 triple16) -> rule1) OR ((triple1 ((triple10 triple9) -> rule4)) -> rule1))] The cow needs the cow.[(((triple14) -> rule2))] The cow visits the cow.[(((triple11) -> rule7))] @2: The cat visits the cat.[(((triple2 ((triple1 triple16) -> rule1)) -> rule4) OR ((triple2 ((triple1 ((triple10 triple9) -> rule4)) -> rule1)) -> rule4))] @3: The cat needs the cat.[(((((triple2 ((triple1 triple16) -> rule1)) -> rule4)) -> rule8) OR ((((triple2 ((triple1 ((triple10 triple9) -> rule4)) -> rule1)) -> rule4)) -> rule8))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
((triple14 triple9) -> (rule5 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
((((triple2 ((triple1 triple16) -> (rule1 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple2 ((triple1 ((triple10 triple9) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple3) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The cow visits the cat.
("cow" "visits" "cat" "+")
int4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat needs the cow.
("cat" "needs" "cow" "+")
triple7
((triple6) -> (rule2 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
triple8
((triple3) -> (rule7 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple9
The cow is big.
("cow" "is" "big" "+")
triple10
The cow is cold.
("cow" "is" "cold" "+")
triple11
The cow is green.
("cow" "is" "green" "+")
triple12
((triple16 triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((triple10 triple9) -> (rule4 % int2)) triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cow is red.
("cow" "is" "red" "+")
triple13
The cow is rough.
("cow" "is" "rough" "+")
triple14
The cow needs the cat.
("cow" "needs" "cat" "+")
triple15
((triple16) -> (rule8 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((triple16 triple1) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((((triple10 triple9) -> (rule4 % int2))) -> (rule8 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
((((triple10 triple9) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
((((triple2 ((triple1 triple16) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple2 ((triple1 ((triple10 triple9) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The cow visits the cat.
("cow" "visits" "cat" "+")
int4
The cow visits the cat.
("cow" "visits" "cat" "+")
triple16
((triple10 triple9) -> (rule4 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple1 triple16) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
((triple1 ((triple10 triple9) -> (rule4 % int2))) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple14) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple11) -> (rule7 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple2 ((triple1 triple16) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
((triple2 ((triple1 ((triple10 triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
int3
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple2 ((triple1 triple16) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple2 ((triple1 ((triple10 triple9) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The cow visits the cat.
("cow" "visits" "cat" "+")
int4