The dog is big. The dog is rough. The dog is round. The dog needs the tiger. The dog sees the tiger. The tiger needs the dog. The tiger sees the dog. If something sees the tiger then the tiger eats the dog. If something eats the tiger and the tiger sees the dog then it is cold.
The dog is big.
("dog" "is" "big" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something sees the tiger then the tiger eats the dog.
((("something" "sees" "tiger" "+")) -> ("tiger" "eats" "dog" "+"))
If something eats the tiger and the tiger sees the dog then it is cold.
((("something" "eats" "tiger" "+") ("tiger" "sees" "dog" "+")) -> ("something" "is" "cold" "+"))
The tiger needs the dog.
True
1
proof
[(triple6)]
("tiger" "needs" "dog" "+")
triple6
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The tiger eats the dog.
True
2
proof
[(((triple5) -> rule1))]
("tiger" "eats" "dog" "+")
((triple5) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger does not eat the dog.
False
2
inv-proof
[(((triple5) -> rule1))]
("tiger" "eats" "dog" "-")
((triple5) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "cold" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "cold" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is big.[(triple1)] The dog is rough.[(triple2)] The dog is round.[(triple3)] The dog needs the tiger.[(triple4)] The dog sees the tiger.[(triple5)] The tiger needs the dog.[(triple6)] The tiger sees the dog.[(triple7)] @1: The tiger eats the dog.[(((triple5) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple5
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple6
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple7
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((triple5) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1