The cat is big. The cat is green. The cat is nice. The cat is red. The cat is rough. The cat needs the rabbit. The cat sees the rabbit. The cat visits the rabbit. The rabbit is green. The rabbit sees the cat. If something is rough then it visits the cat. If something visits the cat then it sees the cat.
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If something is rough then it visits the cat.
((("something" "is" "rough" "+")) -> ("something" "visits" "cat" "+"))
If something visits the cat then it sees the cat.
((("something" "visits" "cat" "+")) -> ("something" "sees" "cat" "+"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The cat is not green.
False
1
inv-proof
[(triple2)]
("cat" "is" "green" "-")
triple2
The cat visits the cat.
True
2
proof
[(((triple5) -> rule1))]
("cat" "visits" "cat" "+")
((triple5) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple5) -> rule1))]
("cat" "visits" "cat" "-")
((triple5) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the cat.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("cat" "sees" "cat" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat does not see the cat.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule2))]
("cat" "sees" "cat" "-")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The rabbit does not visit the cat.
Unknown
inv-rconc
[@1: The rabbit visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not need the cat.
Unknown
inv-random
[@0: The rabbit needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cat" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The cat is big.[(triple1)] The cat is green.[(triple2)] The cat is nice.[(triple3)] The cat is red.[(triple4)] The cat is rough.[(triple5)] The cat needs the rabbit.[(triple6)] The cat sees the rabbit.[(triple7)] The cat visits the rabbit.[(triple8)] The rabbit is green.[(triple9)] The rabbit sees the cat.[(triple10)] @1: The cat visits the cat.[(((triple5) -> rule1))] @2: The cat sees the cat.[(((((triple5) -> rule1)) -> rule2))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple7
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple10
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple5) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2