The cat chases the tiger. The cat is big. The cat is green. The cat is red. The cat is rough. The cat likes the tiger. The cat sees the tiger. The tiger chases the cat. The tiger is big. The tiger sees the cat. If the tiger likes the cat then the tiger sees the cat. If something chases the tiger and it likes the cat then the cat chases the tiger. If something sees the tiger and the tiger chases the cat then the tiger is green. If something chases the tiger then the tiger is big. If something chases the cat then it sees the cat. Kind, big things are rough.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If the tiger likes the cat then the tiger sees the cat.
((("tiger" "likes" "cat" "+")) -> ("tiger" "sees" "cat" "+"))
If something chases the tiger and it likes the cat then the cat chases the tiger.
((("something" "chases" "tiger" "+") ("something" "likes" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If something sees the tiger and the tiger chases the cat then the tiger is green.
((("something" "sees" "tiger" "+") ("tiger" "chases" "cat" "+")) -> ("tiger" "is" "green" "+"))
If something chases the tiger then the tiger is big.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If something chases the cat then it sees the cat.
((("something" "chases" "cat" "+")) -> ("something" "sees" "cat" "+"))
Kind, big things are rough.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
The tiger is big.
True
1
proof
[(triple9 OR ((triple1) -> rule4))]
("tiger" "is" "big" "+")
triple9
((triple1) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The cat is not big.
False
1
inv-proof
[(triple2)]
("cat" "is" "big" "-")
triple2
The tiger is green.
True
3
proof
[(((triple7 triple8) -> rule3))]
("tiger" "is" "green" "+")
((triple7 triple8) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
3
inv-proof
[(((triple7 triple8) -> rule3))]
("tiger" "is" "green" "-")
((triple7 triple8) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "rough" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "cat" "+")
The tiger does not like the cat.
Unknown
inv-random
[@0: The tiger likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cat" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The cat is big.[(triple2)] The cat is green.[(triple3)] The cat is red.[(triple4)] The cat is rough.[(triple5)] The cat likes the tiger.[(triple6)] The cat sees the tiger.[(triple7)] The tiger chases the cat.[(triple8)] The tiger is big.[(triple9 OR ((triple1) -> rule4))] The tiger sees the cat.[(triple10 OR ((triple8) -> rule5))] @1: The tiger is green.[(((triple7 triple8) -> rule3))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple6
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple7
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
((triple1) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple10
((triple8) -> (rule5 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple7 triple8) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1