The cat is big. The cat sees the lion. The cat visits the lion. The cow is big. The cow is round. The cow needs the mouse. The cow visits the cat. The lion is big. The lion needs the mouse. The lion sees the cow. The lion visits the cat. The lion visits the cow. The mouse is big. The mouse is round. The mouse is young. The mouse visits the cat. If something is big and red then it visits the mouse. If something is young then it visits the cow. If something needs the mouse and it needs the cat then the cat is round.
The cat is big.
("cat" "is" "big" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The lion is big.
("lion" "is" "big" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If something is big and red then it visits the mouse.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "visits" "mouse" "+"))
If something is young then it visits the cow.
((("something" "is" "young" "+")) -> ("something" "visits" "cow" "+"))
If something needs the mouse and it needs the cat then the cat is round.
((("something" "needs" "mouse" "+") ("something" "needs" "cat" "+")) -> ("cat" "is" "round" "+"))
The lion is big.
True
1
proof
[(triple8)]
("lion" "is" "big" "+")
triple8
The cow is not round.
False
1
inv-proof
[(triple5)]
("cow" "is" "round" "-")
triple5
The mouse visits the cow.
True
2
proof
[(((triple15) -> rule2))]
("mouse" "visits" "cow" "+")
((triple15) -> (rule2 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The mouse does not visit the cow.
False
2
inv-proof
[(((triple15) -> rule2))]
("mouse" "visits" "cow" "-")
((triple15) -> (rule2 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1
The cat does not visit the mouse.
Unknown
inv-rconc
[@1: The cat visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "mouse" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The cat does not need the lion.
Unknown
inv-random
[@0: The cat needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "lion" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is big.[(triple1)] The cat sees the lion.[(triple2)] The cat visits the lion.[(triple3)] The cow is big.[(triple4)] The cow is round.[(triple5)] The cow needs the mouse.[(triple6)] The cow visits the cat.[(triple7)] The lion is big.[(triple8)] The lion needs the mouse.[(triple9)] The lion sees the cow.[(triple10)] The lion visits the cat.[(triple11)] The lion visits the cow.[(triple12)] The mouse is big.[(triple13)] The mouse is round.[(triple14)] The mouse is young.[(triple15)] The mouse visits the cat.[(triple16)] @1: The mouse visits the cow.[(((triple15) -> rule2))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple6
The cow visits the cat.
("cow" "visits" "cat" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple9
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10
The lion visits the cat.
("lion" "visits" "cat" "+")
triple11
The lion visits the cow.
("lion" "visits" "cow" "+")
triple12
The mouse is big.
("mouse" "is" "big" "+")
triple13
The mouse is round.
("mouse" "is" "round" "+")
triple14
The mouse is young.
("mouse" "is" "young" "+")
triple15
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple16
The mouse visits the cow.
("mouse" "visits" "cow" "+")
((triple15) -> (rule2 % int1))
The mouse visits the cow.
("mouse" "visits" "cow" "+")
int1