The dog is big. The dog is cold. The dog likes the mouse. The dog visits the mouse. The dog visits the tiger. The mouse is big. The mouse is cold. The mouse is green. The mouse likes the tiger. The mouse visits the dog. The tiger does not eat the mouse. The tiger is big. The tiger is nice. The tiger likes the mouse. The tiger visits the dog. The tiger visits the mouse. If something is nice then it likes the mouse. All green things are nice. If the mouse is rough and the mouse does not eat the dog then the mouse visits the tiger.
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something is nice then it likes the mouse.
((("something" "is" "nice" "+")) -> ("something" "likes" "mouse" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If the mouse is rough and the mouse does not eat the dog then the mouse visits the tiger.
((("mouse" "is" "rough" "+") ("mouse" "eats" "dog" "~")) -> ("mouse" "visits" "tiger" "+"))
The mouse is big.
True
1
proof
[(triple6)]
("mouse" "is" "big" "+")
triple6
The mouse is not cold.
False
1
inv-proof
[(triple7)]
("mouse" "is" "cold" "-")
triple7
The mouse is nice.
True
2
proof
[(((triple8) -> rule2))]
("mouse" "is" "nice" "+")
((triple8) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple8) -> rule2))]
("mouse" "is" "nice" "-")
((triple8) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse likes the mouse.
True
3
proof
[(((((triple8) -> rule2)) -> rule1))]
("mouse" "likes" "mouse" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse does not like the mouse.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule1))]
("mouse" "likes" "mouse" "-")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "nice" "-")
The mouse visits the tiger.
Unknown
rconc
[@1: The mouse visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "tiger" "+")
The tiger does not like the dog.
Unknown
inv-random
[@0: The tiger likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "dog" "-")
The tiger eats the dog.
Unknown
random
[@0: The tiger eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "dog" "+")
The dog does not eat the mouse.
Unknown
inv-random
[@0: The dog eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "mouse" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The dog is big.[(triple1)] The dog is cold.[(triple2)] The dog likes the mouse.[(triple3)] The dog visits the mouse.[(triple4)] The dog visits the tiger.[(triple5)] The mouse is big.[(triple6)] The mouse is cold.[(triple7)] The mouse is green.[(triple8)] The mouse likes the tiger.[(triple9)] The mouse visits the dog.[(triple10)] The tiger does not eat the mouse.[(triple11)] The tiger is big.[(triple12)] The tiger is nice.[(triple13)] The tiger likes the mouse.[(triple14 OR ((triple13) -> rule1))] The tiger visits the dog.[(triple15)] The tiger visits the mouse.[(triple16)] @1: The mouse is nice.[(((triple8) -> rule2))] @2: The mouse likes the mouse.[(((((triple8) -> rule2)) -> rule1))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple3
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple4
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple9
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple10
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
triple11
The tiger is big.
("tiger" "is" "big" "+")
triple12
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple14
((triple13) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
The mouse is nice.
("mouse" "is" "nice" "+")
((triple8) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2