The cow eats the dog. The cow eats the mouse. The cow is big. The cow does not visit the mouse. The dog does not eat the cow. The dog is not big. The dog is blue. The dog is cold. The dog is young. The dog sees the cow. The mouse does not eat the cow. The mouse is blue. The mouse is green. The mouse does not see the cow. The mouse does not see the dog. The mouse does not visit the cow. If the cow is green then the cow eats the mouse. If someone sees the cow then the cow does not see the dog. If someone visits the dog and the dog is blue then the dog visits the mouse. If the cow does not visit the mouse then the cow visits the dog. If someone is young and they do not visit the dog then they eat the mouse. If someone eats the mouse and the mouse eats the dog then the dog is young.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is big.
("cow" "is" "big" "+")
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
The dog does not eat the cow.
("dog" "eats" "cow" "-")
The dog is not big.
("dog" "is" "big" "-")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
The mouse does not see the dog.
("mouse" "sees" "dog" "-")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
If the cow is green then the cow eats the mouse.
((("cow" "is" "green" "+")) -> ("cow" "eats" "mouse" "+"))
If someone sees the cow then the cow does not see the dog.
((("someone" "sees" "cow" "+")) -> ("cow" "sees" "dog" "-"))
If someone visits the dog and the dog is blue then the dog visits the mouse.
((("someone" "visits" "dog" "+") ("dog" "is" "blue" "+")) -> ("dog" "visits" "mouse" "+"))
If the cow does not visit the mouse then the cow visits the dog.
((("cow" "visits" "mouse" "~")) -> ("cow" "visits" "dog" "+"))
If someone is young and they do not visit the dog then they eat the mouse.
((("someone" "is" "young" "+") ("someone" "visits" "dog" "~")) -> ("someone" "eats" "mouse" "+"))
If someone eats the mouse and the mouse eats the dog then the dog is young.
((("someone" "eats" "mouse" "+") ("mouse" "eats" "dog" "+")) -> ("dog" "is" "young" "+"))
The dog does not eat the cow.
True
1
proof
[(triple5)]
("dog" "eats" "cow" "-")
triple5
The cow is not big.
False
1
inv-proof
[(triple3)]
("cow" "is" "big" "-")
triple3
The cow does not see the dog.
True
2
proof
[(((triple10) -> rule2))]
("cow" "sees" "dog" "-")
((triple10) -> (rule2 % int1))
The cow does not see the dog.
("cow" "sees" "dog" "-")
int1
The cow does not visit the dog.
False
2
inv-proof
[(((triple4) -> rule4))]
("cow" "visits" "dog" "-")
((triple4) -> (rule4 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog visits the mouse.
True
4
proof
[(((((triple4) -> rule4) triple7) -> rule3))]
("dog" "visits" "mouse" "+")
((((triple4) -> (rule4 % int2)) triple7) -> (rule3 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The dog does not visit the mouse.
False
4
inv-proof
[(((((triple4) -> rule4) triple7) -> rule3))]
("dog" "visits" "mouse" "-")
((((triple4) -> (rule4 % int2)) triple7) -> (rule3 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The dog does not eat the mouse.
Unknown
inv-rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "mouse" "-")
The mouse eats the mouse.
Unknown
rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow does not visit the mouse.[(triple4)] The cow eats the dog.[(triple1)] The cow eats the mouse.[(triple2)] The cow is big.[(triple3)] The dog does not eat the cow.[(triple5)] The dog is blue.[(triple7)] The dog is cold.[(triple8)] The dog is not big.[(triple6)] The dog is young.[(triple9)] The dog sees the cow.[(triple10)] The mouse does not eat the cow.[(triple11)] The mouse does not see the cow.[(triple14)] The mouse does not see the dog.[(triple15)] The mouse does not visit the cow.[(triple16)] The mouse is blue.[(triple12)] The mouse is green.[(triple13)] @1: The cow does not see the dog.[(((triple10) -> rule2))] The cow visits the dog.[(((triple4) -> rule4))] @2: The dog visits the mouse.[(((((triple4) -> rule4) triple7) -> rule3))]
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
triple4
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The dog does not eat the cow.
("dog" "eats" "cow" "-")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple7
The dog is cold.
("dog" "is" "cold" "+")
triple8
The dog is not big.
("dog" "is" "big" "-")
triple6
The dog is young.
("dog" "is" "young" "+")
triple9
The dog sees the cow.
("dog" "sees" "cow" "+")
triple10
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
triple11
The mouse does not see the cow.
("mouse" "sees" "cow" "-")
triple14
The mouse does not see the dog.
("mouse" "sees" "dog" "-")
triple15
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple16
The mouse is blue.
("mouse" "is" "blue" "+")
triple12
The mouse is green.
("mouse" "is" "green" "+")
triple13
The cow does not see the dog.
("cow" "sees" "dog" "-")
((triple10) -> (rule2 % int1))
The cow does not see the dog.
("cow" "sees" "dog" "-")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
((triple4) -> (rule4 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((((triple4) -> (rule4 % int2)) triple7) -> (rule3 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2