The cow sees the dog. The dog needs the cow. The tiger is round. If someone sees the cow and the cow eats the dog then the cow sees the dog. If someone needs the cow then the cow sees the tiger. If someone needs the cow and the cow sees the tiger then the tiger eats the dog. If someone sees the tiger and the tiger eats the dog then the dog sees the cow. If someone is big then they are cold. If someone sees the cow and the cow is cold then the cow needs the dog. If someone needs the tiger and they are cold then they are young. If someone eats the dog then the dog sees the tiger.
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone sees the cow and the cow eats the dog then the cow sees the dog.
((("someone" "sees" "cow" "+") ("cow" "eats" "dog" "+")) -> ("cow" "sees" "dog" "+"))
If someone needs the cow then the cow sees the tiger.
((("someone" "needs" "cow" "+")) -> ("cow" "sees" "tiger" "+"))
If someone needs the cow and the cow sees the tiger then the tiger eats the dog.
((("someone" "needs" "cow" "+") ("cow" "sees" "tiger" "+")) -> ("tiger" "eats" "dog" "+"))
If someone sees the tiger and the tiger eats the dog then the dog sees the cow.
((("someone" "sees" "tiger" "+") ("tiger" "eats" "dog" "+")) -> ("dog" "sees" "cow" "+"))
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the cow and the cow is cold then the cow needs the dog.
((("someone" "sees" "cow" "+") ("cow" "is" "cold" "+")) -> ("cow" "needs" "dog" "+"))
If someone needs the tiger and they are cold then they are young.
((("someone" "needs" "tiger" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone eats the dog then the dog sees the tiger.
((("someone" "eats" "dog" "+")) -> ("dog" "sees" "tiger" "+"))
The dog needs the cow.
True
1
proof
[(triple2)]
("dog" "needs" "cow" "+")
triple2
The dog does not need the cow.
False
1
inv-proof
[(triple2)]
("dog" "needs" "cow" "-")
triple2
The cow sees the tiger.
True
2
proof
[(((triple2) -> rule2))]
("cow" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not see the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "sees" "tiger" "-")
((triple2) -> (rule2 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The tiger eats the dog.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("tiger" "eats" "dog" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The tiger does not eat the dog.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule3))]
("tiger" "eats" "dog" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "young" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "cold" "+")
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "is" "young" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow sees the dog.[(triple1)] The dog needs the cow.[(triple2)] The tiger is round.[(triple3)] @1: The cow sees the tiger.[(((triple2) -> rule2))] @2: The tiger eats the dog.[(((triple2 ((triple2) -> rule2)) -> rule3))] @3: The dog sees the cow.[(((((triple2) -> rule2) ((triple2 ((triple2) -> rule2)) -> rule3)) -> rule4) OR ((((((triple2 ((triple2) -> rule2)) -> rule3)) -> rule8) ((triple2 ((triple2) -> rule2)) -> rule3)) -> rule4))] The dog sees the tiger.[(((((triple2 ((triple2) -> rule2)) -> rule3)) -> rule8))]
The cow sees the dog.
("cow" "sees" "dog" "+")
triple1
The dog needs the cow.
("dog" "needs" "cow" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
((((triple2) -> (rule2 % int3)) ((triple2 ((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int3
((((((triple2 ((triple2) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule8 % int2)) ((triple2 ((triple2) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int2
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int3