The cat is cold. The cat is green. The cat is young. The cat sees the mouse. The cow eats the cat. The cow eats the mouse. The cow is blue. The cow sees the cat. The cow visits the cat. The cow does not visit the mouse. The mouse eats the cow. The mouse is young. If the cat is green and the cat sees the cow then the cow does not eat the mouse. If the cow visits the mouse then the cow does not eat the mouse. If something eats the mouse and the mouse eats the cow then it sees the mouse. If something visits the cat then the cat does not see the cow. If the cow eats the cat and the cat sees the cow then the cat does not eat the mouse. If something visits the cat then it sees the cow.
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is young.
("mouse" "is" "young" "+")
If the cat is green and the cat sees the cow then the cow does not eat the mouse.
((("cat" "is" "green" "+") ("cat" "sees" "cow" "+")) -> ("cow" "eats" "mouse" "-"))
If the cow visits the mouse then the cow does not eat the mouse.
((("cow" "visits" "mouse" "+")) -> ("cow" "eats" "mouse" "-"))
If something eats the mouse and the mouse eats the cow then it sees the mouse.
((("something" "eats" "mouse" "+") ("mouse" "eats" "cow" "+")) -> ("something" "sees" "mouse" "+"))
If something visits the cat then the cat does not see the cow.
((("something" "visits" "cat" "+")) -> ("cat" "sees" "cow" "-"))
If the cow eats the cat and the cat sees the cow then the cat does not eat the mouse.
((("cow" "eats" "cat" "+") ("cat" "sees" "cow" "+")) -> ("cat" "eats" "mouse" "-"))
If something visits the cat then it sees the cow.
((("something" "visits" "cat" "+")) -> ("something" "sees" "cow" "+"))
The cow visits the cat.
True
1
proof
[(triple9)]
("cow" "visits" "cat" "+")
triple9
The cow is not blue.
False
1
inv-proof
[(triple7)]
("cow" "is" "blue" "-")
triple7
The cow sees the mouse.
True
3
proof
[(((triple6 triple11) -> rule3))]
("cow" "sees" "mouse" "+")
((triple6 triple11) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cat sees the cow.
False
2
inv-proof
[(((triple9) -> rule4))]
("cat" "sees" "cow" "+")
((triple9) -> (rule4 % int1))
The cat does not see the cow.
("cat" "sees" "cow" "-")
int1
The mouse does not see the cow.
Unknown
inv-rconc
[@1: The mouse sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "cow" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not visit the cow.
Unknown
inv-random
[@0: The mouse visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cow" "-")
The cat eats the mouse.
Unknown
random
[@0: The cat eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "mouse" "+")
@0: The cat is cold.[(triple1)] The cat is green.[(triple2)] The cat is young.[(triple3)] The cat sees the mouse.[(triple4)] The cow does not visit the mouse.[(triple10)] The cow eats the cat.[(triple5)] The cow eats the mouse.[(triple6)] The cow is blue.[(triple7)] The cow sees the cat.[(triple8)] The cow visits the cat.[(triple9)] The mouse eats the cow.[(triple11)] The mouse is young.[(triple12)] @1: The cat does not see the cow.[(((triple9) -> rule4))] The cow sees the cow.[(((triple9) -> rule6))] The cow sees the mouse.[(((triple6 triple11) -> rule3))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple4
The cow does not visit the mouse.
("cow" "visits" "mouse" "-")
triple10
The cow eats the cat.
("cow" "eats" "cat" "+")
triple5
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple6
The cow is blue.
("cow" "is" "blue" "+")
triple7
The cow sees the cat.
("cow" "sees" "cat" "+")
triple8
The cow visits the cat.
("cow" "visits" "cat" "+")
triple9
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple12
The cat does not see the cow.
("cat" "sees" "cow" "-")
((triple9) -> (rule4 % int1))
The cat does not see the cow.
("cat" "sees" "cow" "-")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple9) -> (rule6 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((triple6 triple11) -> (rule3 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1