The cow chases the dog. The cow is green. The cow does not need the dog. The cow needs the tiger. The cow sees the tiger. The dog is blue. The dog is green. The dog needs the tiger. The dog sees the cow. The tiger is blue. The tiger is cold. The tiger is green. The tiger is kind. The tiger needs the cow. The tiger does not need the dog. The tiger sees the dog. If someone sees the tiger then they are round.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is green.
("cow" "is" "green" "+")
The cow does not need the dog.
("cow" "needs" "dog" "-")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If someone sees the tiger then they are round.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "round" "+"))
The tiger is blue.
True
1
proof
[(triple10)]
("tiger" "is" "blue" "+")
triple10
The tiger is not kind.
False
1
inv-proof
[(triple13)]
("tiger" "is" "kind" "-")
triple13
The cow is round.
True
2
proof
[(((triple5) -> rule1))]
("cow" "is" "round" "+")
((triple5) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple5) -> rule1))]
("cow" "is" "round" "-")
((triple5) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The tiger is not round.
Unknown
inv-rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "round" "-")
The dog is round.
Unknown
rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "round" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow chases the dog.[(triple1)] The cow does not need the dog.[(triple3)] The cow is green.[(triple2)] The cow needs the tiger.[(triple4)] The cow sees the tiger.[(triple5)] The dog is blue.[(triple6)] The dog is green.[(triple7)] The dog needs the tiger.[(triple8)] The dog sees the cow.[(triple9)] The tiger does not need the dog.[(triple15)] The tiger is blue.[(triple10)] The tiger is cold.[(triple11)] The tiger is green.[(triple12)] The tiger is kind.[(triple13)] The tiger needs the cow.[(triple14)] The tiger sees the dog.[(triple16)] @1: The cow is round.[(((triple5) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow does not need the dog.
("cow" "needs" "dog" "-")
triple3
The cow is green.
("cow" "is" "green" "+")
triple2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple4
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog is green.
("dog" "is" "green" "+")
triple7
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple8
The dog sees the cow.
("dog" "sees" "cow" "+")
triple9
The tiger does not need the dog.
("tiger" "needs" "dog" "-")
triple15
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple14
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple16
The cow is round.
("cow" "is" "round" "+")
((triple5) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1