The cat eats the tiger. The dog needs the cat. The mouse is not rough. The tiger eats the dog. If the mouse sees the cat and the dog does not need the mouse then the dog is red. If something is red and it does not see the mouse then the mouse is not big. If something needs the cat and it eats the dog then it is rough. If something needs the cat then it eats the dog. If something sees the cat then the cat is green. If something sees the mouse and it sees the cat then the mouse eats the dog.
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
If the mouse sees the cat and the dog does not need the mouse then the dog is red.
((("mouse" "sees" "cat" "+") ("dog" "needs" "mouse" "~")) -> ("dog" "is" "red" "+"))
If something is red and it does not see the mouse then the mouse is not big.
((("something" "is" "red" "+") ("something" "sees" "mouse" "~")) -> ("mouse" "is" "big" "-"))
If something needs the cat and it eats the dog then it is rough.
((("something" "needs" "cat" "+") ("something" "eats" "dog" "+")) -> ("something" "is" "rough" "+"))
If something needs the cat then it eats the dog.
((("something" "needs" "cat" "+")) -> ("something" "eats" "dog" "+"))
If something sees the cat then the cat is green.
((("something" "sees" "cat" "+")) -> ("cat" "is" "green" "+"))
If something sees the mouse and it sees the cat then the mouse eats the dog.
((("something" "sees" "mouse" "+") ("something" "sees" "cat" "+")) -> ("mouse" "eats" "dog" "+"))
The dog needs the cat.
True
1
proof
[(triple2)]
("dog" "needs" "cat" "+")
triple2
The mouse is rough.
False
1
inv-proof
[(triple3)]
("mouse" "is" "rough" "+")
triple3
The dog eats the dog.
True
2
proof
[(((triple2) -> rule4))]
("dog" "eats" "dog" "+")
((triple2) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog does not eat the dog.
False
2
inv-proof
[(((triple2) -> rule4))]
("dog" "eats" "dog" "-")
((triple2) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is rough.
True
4
proof
[(((triple2 ((triple2) -> rule4)) -> rule3))]
("dog" "is" "rough" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The dog is not rough.
False
4
inv-proof
[(((triple2 ((triple2) -> rule4)) -> rule3))]
("dog" "is" "rough" "-")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The mouse does not eat the dog.
Unknown
inv-rconc
[@1: The mouse eats the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "eats" "dog" "-")
The cat is green.
Unknown
rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "green" "+")
The cat does not eat the dog.
Unknown
inv-rconc
[@1: The cat eats the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "dog" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not see the dog.
Unknown
inv-random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "-")
The tiger needs the mouse.
Unknown
random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "+")
@0: The cat eats the tiger.[(triple1)] The dog needs the cat.[(triple2)] The mouse is not rough.[(triple3)] The tiger eats the dog.[(triple4)] @1: The dog eats the dog.[(((triple2) -> rule4))] @2: The dog is rough.[(((triple2 ((triple2) -> rule4)) -> rule3))]
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple2
The mouse is not rough.
("mouse" "is" "rough" "-")
triple3
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple4
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple2) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2