The cow chases the dog. The cow is red. The cow sees the dog. The dog chases the cow. The dog is big. The dog needs the cow. The dog sees the cow. If someone chases the dog and the dog sees the cow then they are big. If someone is blue then they chase the dog. If someone is big and red then they see the cow. If someone is blue and they see the cow then they need the cow. If someone sees the cow and they need the dog then they are young. If the cow chases the dog and the cow sees the dog then the cow needs the dog. If someone needs the cow then the cow sees the dog. If someone chases the cow then the cow sees the dog.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog is big.
("dog" "is" "big" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If someone chases the dog and the dog sees the cow then they are big.
((("someone" "chases" "dog" "+") ("dog" "sees" "cow" "+")) -> ("someone" "is" "big" "+"))
If someone is blue then they chase the dog.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "dog" "+"))
If someone is big and red then they see the cow.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "sees" "cow" "+"))
If someone is blue and they see the cow then they need the cow.
((("someone" "is" "blue" "+") ("someone" "sees" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If someone sees the cow and they need the dog then they are young.
((("someone" "sees" "cow" "+") ("someone" "needs" "dog" "+")) -> ("someone" "is" "young" "+"))
If the cow chases the dog and the cow sees the dog then the cow needs the dog.
((("cow" "chases" "dog" "+") ("cow" "sees" "dog" "+")) -> ("cow" "needs" "dog" "+"))
If someone needs the cow then the cow sees the dog.
((("someone" "needs" "cow" "+")) -> ("cow" "sees" "dog" "+"))
If someone chases the cow then the cow sees the dog.
((("someone" "chases" "cow" "+")) -> ("cow" "sees" "dog" "+"))
The dog is big.
True
1
proof
[(triple5)]
("dog" "is" "big" "+")
triple5
The cow does not see the dog.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule8) OR ((triple6) -> rule7))]
("cow" "sees" "dog" "-")
triple3
((triple4) -> (rule8 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
((triple6) -> (rule7 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow is big.
True
3
proof
[(((triple1 triple7) -> rule1))]
("cow" "is" "big" "+")
((triple1 triple7) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is not big.
False
3
inv-proof
[(((triple1 triple7) -> rule1))]
("cow" "is" "big" "-")
((triple1 triple7) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "needs" "cow" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "young" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cow chases the dog.[(triple1)] The cow is red.[(triple2)] The cow sees the dog.[(triple3 OR ((triple4) -> rule8) OR ((triple6) -> rule7))] The dog chases the cow.[(triple4)] The dog is big.[(triple5)] The dog needs the cow.[(triple6)] The dog sees the cow.[(triple7)] @1: The cow is big.[(((triple1 triple7) -> rule1))] The cow needs the dog.[(((triple1 triple3) -> rule6) OR ((triple1 ((triple4) -> rule8)) -> rule6) OR ((triple1 ((triple6) -> rule7)) -> rule6))] @2: The cow sees the cow.[(((((triple1 triple7) -> rule1) triple2) -> rule3))] @3: The cow is young.[(((((((triple1 triple7) -> rule1) triple2) -> rule3) ((triple1 triple3) -> rule6)) -> rule5) OR ((((((triple1 triple7) -> rule1) triple2) -> rule3) ((triple1 ((triple4) -> rule8)) -> rule6)) -> rule5) OR ((((((triple1 triple7) -> rule1) triple2) -> rule3) ((triple1 ((triple6) -> rule7)) -> rule6)) -> rule5))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
((triple4) -> (rule8 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
((triple6) -> (rule7 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog needs the cow.
("dog" "needs" "cow" "+")
triple6
The dog sees the cow.
("dog" "sees" "cow" "+")
triple7
The cow is big.
("cow" "is" "big" "+")
((triple1 triple7) -> (rule1 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
((triple1 triple3) -> (rule6 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
((triple1 ((triple4) -> (rule8 % int2))) -> (rule6 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
((triple1 ((triple6) -> (rule7 % int2))) -> (rule6 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple1 triple7) -> (rule1 % int2)) triple2) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow is young.
("cow" "is" "young" "+")
((((((triple1 triple7) -> (rule1 % int4)) triple2) -> (rule3 % int3)) ((triple1 triple3) -> (rule6 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow is big.
("cow" "is" "big" "+")
int4
((((((triple1 triple7) -> (rule1 % int5)) triple2) -> (rule3 % int4)) ((triple1 ((triple4) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
The cow is big.
("cow" "is" "big" "+")
int5
((((((triple1 triple7) -> (rule1 % int5)) triple2) -> (rule3 % int4)) ((triple1 ((triple6) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
The cow is big.
("cow" "is" "big" "+")
int5