The cat is big. The cat is blue. The cat is red. The cat likes the rabbit. The cat sees the rabbit. The cat visits the mouse. The mouse is red. The mouse likes the cat. The mouse sees the rabbit. The mouse visits the cat. The rabbit is big. The rabbit is nice. The rabbit is red. The rabbit does not see the cat. The rabbit sees the mouse. The rabbit visits the mouse. If something likes the mouse then the mouse likes the rabbit. All blue things are big. If the mouse does not visit the rabbit then the rabbit is red. If something is round then it likes the mouse. If something is blue then it likes the mouse. If something visits the mouse and the mouse visits the cat then it is round. If something sees the cat and the cat likes the rabbit then it is not blue. If something likes the mouse then the mouse sees the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something likes the mouse then the mouse likes the rabbit.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If the mouse does not visit the rabbit then the rabbit is red.
((("mouse" "visits" "rabbit" "~")) -> ("rabbit" "is" "red" "+"))
If something is round then it likes the mouse.
((("something" "is" "round" "+")) -> ("something" "likes" "mouse" "+"))
If something is blue then it likes the mouse.
((("something" "is" "blue" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the mouse and the mouse visits the cat then it is round.
((("something" "visits" "mouse" "+") ("mouse" "visits" "cat" "+")) -> ("something" "is" "round" "+"))
If something sees the cat and the cat likes the rabbit then it is not blue.
((("something" "sees" "cat" "+") ("cat" "likes" "rabbit" "+")) -> ("something" "is" "blue" "-"))
If something likes the mouse then the mouse sees the cat.
((("something" "likes" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple15)]
("rabbit" "sees" "mouse" "+")
triple15
The rabbit is not red.
False
1
inv-proof
[(triple13)]
("rabbit" "is" "red" "-")
triple13
The cat likes the mouse.
True
2
proof
[(((triple2) -> rule5) OR ((((triple6 triple10) -> rule6)) -> rule4))]
("cat" "likes" "mouse" "+")
((triple2) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
((((triple6 triple10) -> (rule6 % int2))) -> (rule4 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The rabbit is not round.
False
3
inv-proof
[(((triple16 triple10) -> rule6))]
("rabbit" "is" "round" "-")
((triple16 triple10) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The mouse does not like the mouse.
Unknown
inv-rconc
[@2: The mouse likes the mouse.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "round" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The cat is big.[(triple1 OR ((triple2) -> rule2))] The cat is blue.[(triple2)] The cat is red.[(triple3)] The cat likes the rabbit.[(triple4)] The cat sees the rabbit.[(triple5)] The cat visits the mouse.[(triple6)] The mouse is red.[(triple7)] The mouse likes the cat.[(triple8)] The mouse sees the rabbit.[(triple9)] The mouse visits the cat.[(triple10)] The rabbit does not see the cat.[(triple14)] The rabbit is big.[(triple11)] The rabbit is nice.[(triple12)] The rabbit is red.[(triple13)] The rabbit sees the mouse.[(triple15)] The rabbit visits the mouse.[(triple16)] @1: The cat is round.[(((triple6 triple10) -> rule6))] The cat likes the mouse.[(((triple2) -> rule5) OR ((((triple6 triple10) -> rule6)) -> rule4))] The rabbit is round.[(((triple16 triple10) -> rule6))] @2: The mouse likes the rabbit.[(((((triple2) -> rule5)) -> rule1) OR ((((((triple16 triple10) -> rule6)) -> rule4)) -> rule1) OR ((((((triple6 triple10) -> rule6)) -> rule4)) -> rule1))] The mouse sees the cat.[(((((triple2) -> rule5)) -> rule8) OR ((((((triple16 triple10) -> rule6)) -> rule4)) -> rule8) OR ((((((triple6 triple10) -> rule6)) -> rule4)) -> rule8))] The rabbit likes the mouse.[(((((triple16 triple10) -> rule6)) -> rule4))] @3: The mouse is not blue.[(((((((triple2) -> rule5)) -> rule8) triple4) -> rule7) OR ((((((((triple16 triple10) -> rule6)) -> rule4)) -> rule8) triple4) -> rule7) OR ((((((((triple6 triple10) -> rule6)) -> rule4)) -> rule8) triple4) -> rule7))]
The cat is big.
("cat" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple4
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple5
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple8
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple9
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple10
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple14
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple12
The rabbit is red.
("rabbit" "is" "red" "+")
triple13
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple16
The cat is round.
("cat" "is" "round" "+")
((triple6 triple10) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((triple2) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
((((triple6 triple10) -> (rule6 % int2))) -> (rule4 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
((triple16 triple10) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
((((((triple16 triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
((((((triple6 triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
((((((triple16 triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
((((((triple6 triple10) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((triple16 triple10) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The mouse is not blue.
("mouse" "is" "blue" "-")
((((((triple2) -> (rule5 % int3))) -> (rule8 % int2)) triple4) -> (rule7 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int3
((((((((triple16 triple10) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple4) -> (rule7 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
((((((((triple6 triple10) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) triple4) -> (rule7 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4