The cow chases the dog. The cow chases the tiger. The cow is young. The dog chases the tiger. The dog is cold. The dog is young. The dog sees the cow. The tiger chases the dog. The tiger is blue. The tiger needs the cow. The tiger sees the cow. The tiger sees the dog. If something chases the dog and it is blue then the dog is blue. If something chases the cow then the cow is young. If something sees the tiger then it sees the cow. If something sees the cow and it needs the cow then it needs the dog. If something is young then it needs the cow. If something is young then it needs the tiger.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is young.
("cow" "is" "young" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something chases the dog and it is blue then the dog is blue.
((("something" "chases" "dog" "+") ("something" "is" "blue" "+")) -> ("dog" "is" "blue" "+"))
If something chases the cow then the cow is young.
((("something" "chases" "cow" "+")) -> ("cow" "is" "young" "+"))
If something sees the tiger then it sees the cow.
((("something" "sees" "tiger" "+")) -> ("something" "sees" "cow" "+"))
If something sees the cow and it needs the cow then it needs the dog.
((("something" "sees" "cow" "+") ("something" "needs" "cow" "+")) -> ("something" "needs" "dog" "+"))
If something is young then it needs the cow.
((("something" "is" "young" "+")) -> ("something" "needs" "cow" "+"))
If something is young then it needs the tiger.
((("something" "is" "young" "+")) -> ("something" "needs" "tiger" "+"))
The tiger sees the cow.
True
1
proof
[(triple11)]
("tiger" "sees" "cow" "+")
triple11
The tiger does not need the cow.
False
1
inv-proof
[(triple10)]
("tiger" "needs" "cow" "-")
triple10
The dog needs the cow.
True
2
proof
[(((triple6) -> rule5))]
("dog" "needs" "cow" "+")
((triple6) -> (rule5 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog does not need the tiger.
False
2
inv-proof
[(((triple6) -> rule6))]
("dog" "needs" "tiger" "-")
((triple6) -> (rule6 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog needs the dog.
True
4
proof
[(((triple7 ((triple6) -> rule5)) -> rule4))]
("dog" "needs" "dog" "+")
((triple7 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The dog does not need the dog.
False
4
inv-proof
[(((triple7 ((triple6) -> rule5)) -> rule4))]
("dog" "needs" "dog" "-")
((triple7 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2
The cow does not need the dog.
Unknown
inv-rconc
[@2: The cow needs the dog.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("cow" "needs" "dog" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "cow" "+")
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The cow sees the tiger.
Unknown
random
[@0: The cow sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "tiger" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The cow chases the dog.[(triple1)] The cow chases the tiger.[(triple2)] The cow is young.[(triple3)] The dog chases the tiger.[(triple4)] The dog is cold.[(triple5)] The dog is young.[(triple6)] The dog sees the cow.[(triple7)] The tiger chases the dog.[(triple8)] The tiger is blue.[(triple9)] The tiger needs the cow.[(triple10)] The tiger sees the cow.[(triple11)] The tiger sees the dog.[(triple12)] @1: The cow needs the cow.[(((triple3) -> rule5))] The cow needs the tiger.[(((triple3) -> rule6))] The dog is blue.[(((triple8 triple9) -> rule1))] The dog needs the cow.[(((triple6) -> rule5))] The dog needs the tiger.[(((triple6) -> rule6))] The tiger needs the dog.[(((triple11 triple10) -> rule4))] @2: The dog needs the dog.[(((triple7 ((triple6) -> rule5)) -> rule4))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
triple3
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The dog sees the cow.
("dog" "sees" "cow" "+")
triple7
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple10
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple11
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple12
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple3) -> (rule5 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((triple3) -> (rule6 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((triple8 triple9) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
((triple6) -> (rule5 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((triple6) -> (rule6 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((triple11 triple10) -> (rule4 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple7 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the cow.
("dog" "needs" "cow" "+")
int2