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