The cat is not rough. The cow is big. The lion likes the cat. The tiger does not see the lion. If something likes the tiger and it likes the cow then the cow likes the lion. If something visits the cat then the cat does not see the lion. If something likes the cat then it does not visit the cow. If something is blue then it visits the cow. If the cat sees the lion and the cat is not big then the cat is rough. If something likes the cat then the cat is red. If something visits the cow then it sees the tiger. If something is red then it visits the cat.
The cat is not rough.
("cat" "is" "rough" "-")
The cow is big.
("cow" "is" "big" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
If something likes the tiger and it likes the cow then the cow likes the lion.
((("something" "likes" "tiger" "+") ("something" "likes" "cow" "+")) -> ("cow" "likes" "lion" "+"))
If something visits the cat then the cat does not see the lion.
((("something" "visits" "cat" "+")) -> ("cat" "sees" "lion" "-"))
If something likes the cat then it does not visit the cow.
((("something" "likes" "cat" "+")) -> ("something" "visits" "cow" "-"))
If something is blue then it visits the cow.
((("something" "is" "blue" "+")) -> ("something" "visits" "cow" "+"))
If the cat sees the lion and the cat is not big then the cat is rough.
((("cat" "sees" "lion" "+") ("cat" "is" "big" "~")) -> ("cat" "is" "rough" "+"))
If something likes the cat then the cat is red.
((("something" "likes" "cat" "+")) -> ("cat" "is" "red" "+"))
If something visits the cow then it sees the tiger.
((("something" "visits" "cow" "+")) -> ("something" "sees" "tiger" "+"))
If something is red then it visits the cat.
((("something" "is" "red" "+")) -> ("something" "visits" "cat" "+"))
The tiger does not see the lion.
True
1
proof
[(triple4)]
("tiger" "sees" "lion" "-")
triple4
The lion does not like the cat.
False
1
inv-proof
[(triple3)]
("lion" "likes" "cat" "-")
triple3
The cat is red.
True
2
proof
[(((triple3) -> rule6))]
("cat" "is" "red" "+")
((triple3) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple3) -> rule6))]
("cat" "is" "red" "-")
((triple3) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat visits the cat.
True
3
proof
[(((((triple3) -> rule6)) -> rule8))]
("cat" "visits" "cat" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat does not visit the cat.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule8))]
("cat" "visits" "cat" "-")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat does not see the lion.
True
4
proof
[(((((((triple3) -> rule6)) -> rule8)) -> rule2))]
("cat" "sees" "lion" "-")
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat does not see the lion.
("cat" "sees" "lion" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat sees the lion.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule8)) -> rule2))]
("cat" "sees" "lion" "+")
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat does not see the lion.
("cat" "sees" "lion" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The tiger does not visit the cat.
Unknown
inv-rconc
[@1: The tiger visits the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "visits" "cat" "-")
The lion sees the tiger.
Unknown
rconc
[@1: The lion sees the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "tiger" "+")
The cow does not like the lion.
Unknown
inv-rconc
[@1: The cow likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "lion" "-")
The cat visits the cow.
Unknown
rconc
[@1: The cat visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "cow" "+")
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 lion sees the cat.
Unknown
random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "+")
The tiger does not like the cow.
Unknown
inv-random
[@0: The tiger likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cow" "-")
The cat likes the lion.
Unknown
random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "+")
@0: The cat is not rough.[(triple1)] The cow is big.[(triple2)] The lion likes the cat.[(triple3)] The tiger does not see the lion.[(triple4)] @1: The cat is red.[(((triple3) -> rule6))] The lion does not visit the cow.[(((triple3) -> rule3))] @2: The cat visits the cat.[(((((triple3) -> rule6)) -> rule8))] @3: The cat does not see the lion.[(((((((triple3) -> rule6)) -> rule8)) -> rule2))]
The cat is not rough.
("cat" "is" "rough" "-")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The lion likes the cat.
("lion" "likes" "cat" "+")
triple3
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
triple4
The cat is red.
("cat" "is" "red" "+")
((triple3) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The lion does not visit the cow.
("lion" "visits" "cow" "-")
((triple3) -> (rule3 % int1))
The lion does not visit the cow.
("lion" "visits" "cow" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat does not see the lion.
("cat" "sees" "lion" "-")
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat does not see the lion.
("cat" "sees" "lion" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3