The cat is round. The cat visits the lion. The dog needs the cat. The dog needs the lion. The dog sees the lion. The lion is big. The lion is not kind. The lion needs the mouse. The lion sees the cat. The lion does not see the dog. The lion visits the dog. The lion does not visit the mouse. The mouse is big. The mouse is round. The mouse is young. The mouse sees the lion. If something needs the lion then the lion visits the cat. If something needs the dog and the dog sees the mouse then it visits the cat. If something visits the lion and it sees the dog then it visits the cat. If something visits the mouse then it is cold. If something needs the cat then it is not cold. If something is big and it visits the cat then the cat visits the mouse. If something visits the mouse and the mouse is young then the mouse sees the cat. If something needs the lion and it visits the cat then the cat does not see the lion.
The cat is round.
("cat" "is" "round" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion does not see the dog.
("lion" "sees" "dog" "-")
The lion visits the dog.
("lion" "visits" "dog" "+")
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something needs the lion then the lion visits the cat.
((("something" "needs" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If something needs the dog and the dog sees the mouse then it visits the cat.
((("something" "needs" "dog" "+") ("dog" "sees" "mouse" "+")) -> ("something" "visits" "cat" "+"))
If something visits the lion and it sees the dog then it visits the cat.
((("something" "visits" "lion" "+") ("something" "sees" "dog" "+")) -> ("something" "visits" "cat" "+"))
If something visits the mouse then it is cold.
((("something" "visits" "mouse" "+")) -> ("something" "is" "cold" "+"))
If something needs the cat then it is not cold.
((("something" "needs" "cat" "+")) -> ("something" "is" "cold" "-"))
If something is big and it visits the cat then the cat visits the mouse.
((("something" "is" "big" "+") ("something" "visits" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If something visits the mouse and the mouse is young then the mouse sees the cat.
((("something" "visits" "mouse" "+") ("mouse" "is" "young" "+")) -> ("mouse" "sees" "cat" "+"))
If something needs the lion and it visits the cat then the cat does not see the lion.
((("something" "needs" "lion" "+") ("something" "visits" "cat" "+")) -> ("cat" "sees" "lion" "-"))
The lion does not visit the mouse.
True
1
proof
[(triple12)]
("lion" "visits" "mouse" "-")
triple12
The lion does not see the cat.
False
1
inv-proof
[(triple9)]
("lion" "sees" "cat" "-")
triple9
The dog is not cold.
True
2
proof
[(((triple3) -> rule5))]
("dog" "is" "cold" "-")
((triple3) -> (rule5 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The lion does not visit the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "visits" "cat" "-")
((triple4) -> (rule1 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat visits the mouse.
True
4
proof
[(((triple6 ((triple4) -> rule1)) -> rule6))]
("cat" "visits" "mouse" "+")
((triple6 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat does not visit the mouse.
False
4
inv-proof
[(((triple6 ((triple4) -> rule1)) -> rule6))]
("cat" "visits" "mouse" "-")
((triple6 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The mouse sees the cat.
True
6
proof
[(((((triple6 ((triple4) -> rule1)) -> rule6) triple15) -> rule7))]
("mouse" "sees" "cat" "+")
((((triple6 ((triple4) -> (rule1 % int3))) -> (rule6 % int2)) triple15) -> (rule7 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat is not cold.
False
5
inv-proof
[(((((triple6 ((triple4) -> rule1)) -> rule6)) -> rule4))]
("cat" "is" "cold" "-")
((((triple6 ((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "cold" "-")
The dog visits the cat.
Unknown
rconc
[@1: The dog visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "visits" "cat" "+")
The mouse does not visit the cat.
Unknown
inv-rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "cat" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "cold" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat sees the dog.
Unknown
random
[@0: The cat sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "dog" "+")
@0: The cat is round.[(triple1)] The cat visits the lion.[(triple2)] The dog needs the cat.[(triple3)] The dog needs the lion.[(triple4)] The dog sees the lion.[(triple5)] The lion does not see the dog.[(triple10)] The lion does not visit the mouse.[(triple12)] The lion is big.[(triple6)] The lion is not kind.[(triple7)] The lion needs the mouse.[(triple8)] The lion sees the cat.[(triple9)] The lion visits the dog.[(triple11)] The mouse is big.[(triple13)] The mouse is round.[(triple14)] The mouse is young.[(triple15)] The mouse sees the lion.[(triple16)] @1: The dog is not cold.[(((triple3) -> rule5))] The lion visits the cat.[(((triple4) -> rule1))] @2: The cat visits the mouse.[(((triple6 ((triple4) -> rule1)) -> rule6))] @3: The cat is cold.[(((((triple6 ((triple4) -> rule1)) -> rule6)) -> rule4))] The mouse sees the cat.[(((((triple6 ((triple4) -> rule1)) -> rule6) triple15) -> rule7))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat visits the lion.
("cat" "visits" "lion" "+")
triple2
The dog needs the cat.
("dog" "needs" "cat" "+")
triple3
The dog needs the lion.
("dog" "needs" "lion" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The lion does not see the dog.
("lion" "sees" "dog" "-")
triple10
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
triple12
The lion is big.
("lion" "is" "big" "+")
triple6
The lion is not kind.
("lion" "is" "kind" "-")
triple7
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple8
The lion sees the cat.
("lion" "sees" "cat" "+")
triple9
The lion visits the dog.
("lion" "visits" "dog" "+")
triple11
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 sees the lion.
("mouse" "sees" "lion" "+")
triple16
The dog is not cold.
("dog" "is" "cold" "-")
((triple3) -> (rule5 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple4) -> (rule1 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
((triple6 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
((((triple6 ((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((((triple6 ((triple4) -> (rule1 % int3))) -> (rule6 % int2)) triple15) -> (rule7 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3