The bear needs the cat. The cat needs the cow. The cow sees the cat. The dog needs the bear. If something sees the cow and the cow is cold then the cow is young. If the cow is not cold then the cow is not round. If something needs the bear and the bear needs the dog then the dog chases the cat. If something needs the dog then it does not chase the cat. If something needs the cat then the cat is young. If something sees the cow and it needs the dog then the cow chases the cat. If something is young then it chases the bear. If the cat needs the cow and the cow is nice then the cat chases the dog.
The bear needs the cat.
("bear" "needs" "cat" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
If something sees the cow and the cow is cold then the cow is young.
((("something" "sees" "cow" "+") ("cow" "is" "cold" "+")) -> ("cow" "is" "young" "+"))
If the cow is not cold then the cow is not round.
((("cow" "is" "cold" "~")) -> ("cow" "is" "round" "-"))
If something needs the bear and the bear needs the dog then the dog chases the cat.
((("something" "needs" "bear" "+") ("bear" "needs" "dog" "+")) -> ("dog" "chases" "cat" "+"))
If something needs the dog then it does not chase the cat.
((("something" "needs" "dog" "+")) -> ("something" "chases" "cat" "-"))
If something needs the cat then the cat is young.
((("something" "needs" "cat" "+")) -> ("cat" "is" "young" "+"))
If something sees the cow and it needs the dog then the cow chases the cat.
((("something" "sees" "cow" "+") ("something" "needs" "dog" "+")) -> ("cow" "chases" "cat" "+"))
If something is young then it chases the bear.
((("something" "is" "young" "+")) -> ("something" "chases" "bear" "+"))
If the cat needs the cow and the cow is nice then the cat chases the dog.
((("cat" "needs" "cow" "+") ("cow" "is" "nice" "+")) -> ("cat" "chases" "dog" "+"))
The cow sees the cat.
True
1
proof
[(triple3)]
("cow" "sees" "cat" "+")
triple3
The dog does not need the bear.
False
1
inv-proof
[(triple4)]
("dog" "needs" "bear" "-")
triple4
The cat is young.
True
2
proof
[(((triple1) -> rule5))]
("cat" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is not young.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "is" "young" "-")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat chases the bear.
True
3
proof
[(((((triple1) -> rule5)) -> rule7))]
("cat" "chases" "bear" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat does not chase the bear.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule7))]
("cat" "chases" "bear" "-")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The dog does not chase the bear.
Unknown
inv-rconc
[@1: The dog chases the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "chases" "bear" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "chases" "bear" "+")
The cow does not chase the bear.
Unknown
inv-rconc
[@2: The cow chases the bear.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("cow" "chases" "bear" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The dog does not see the cow.
Unknown
inv-random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "-")
The bear sees the dog.
Unknown
random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "+")
@0: The bear needs the cat.[(triple1)] The cat needs the cow.[(triple2)] The cow sees the cat.[(triple3)] The dog needs the bear.[(triple4)] @1: The cat is young.[(((triple1) -> rule5))] @2: The cat chases the bear.[(((((triple1) -> rule5)) -> rule7))]
The bear needs the cat.
("bear" "needs" "cat" "+")
triple1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple2
The cow sees the cat.
("cow" "sees" "cat" "+")
triple3
The dog needs the bear.
("dog" "needs" "bear" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
((triple1) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
((((triple1) -> (rule5 % int2))) -> (rule7 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2