The cat is cold. The cow is rough. The dog likes the tiger. The dog visits the tiger. The tiger is cold. The tiger is rough. The tiger likes the cat. The tiger likes the cow. The tiger sees the cat. The tiger sees the dog. The tiger visits the cow. The tiger visits the dog. If something visits the tiger and the tiger visits the dog then the dog is kind. Kind things are big.
The cat is cold.
("cat" "is" "cold" "+")
The cow is rough.
("cow" "is" "rough" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something visits the tiger and the tiger visits the dog then the dog is kind.
((("something" "visits" "tiger" "+") ("tiger" "visits" "dog" "+")) -> ("dog" "is" "kind" "+"))
Kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
The dog visits the tiger.
True
1
proof
[(triple4)]
("dog" "visits" "tiger" "+")
triple4
The tiger does not see the dog.
False
1
inv-proof
[(triple10)]
("tiger" "sees" "dog" "-")
triple10
The dog is kind.
True
3
proof
[(((triple4 triple12) -> rule1))]
("dog" "is" "kind" "+")
((triple4 triple12) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is not kind.
False
3
inv-proof
[(((triple4 triple12) -> rule1))]
("dog" "is" "kind" "-")
((triple4 triple12) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is big.
True
4
proof
[(((((triple4 triple12) -> rule1)) -> rule2))]
("dog" "is" "big" "+")
((((triple4 triple12) -> (rule1 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is not big.
False
4
inv-proof
[(((((triple4 triple12) -> rule1)) -> rule2))]
("dog" "is" "big" "-")
((((triple4 triple12) -> (rule1 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "big" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "big" "+")
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "big" "-")
The cat sees the tiger.
Unknown
random
[@0: The cat sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "tiger" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The dog sees the cat.
Unknown
random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "+")
@0: The cat is cold.[(triple1)] The cow is rough.[(triple2)] The dog likes the tiger.[(triple3)] The dog visits the tiger.[(triple4)] The tiger is cold.[(triple5)] The tiger is rough.[(triple6)] The tiger likes the cat.[(triple7)] The tiger likes the cow.[(triple8)] The tiger sees the cat.[(triple9)] The tiger sees the dog.[(triple10)] The tiger visits the cow.[(triple11)] The tiger visits the dog.[(triple12)] @1: The dog is kind.[(((triple4 triple12) -> rule1))] @2: The dog is big.[(((((triple4 triple12) -> rule1)) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple3
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple7
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple8
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple9
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple10
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The dog is kind.
("dog" "is" "kind" "+")
((triple4 triple12) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((((triple4 triple12) -> (rule1 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2