The dog is kind. The dog visits the tiger. The mouse chases the tiger. The mouse is round. The mouse sees the tiger. The tiger chases the dog. The tiger is big. If something sees the tiger then the tiger is red. If something chases the dog and the dog is kind then the dog is round. If something is round then it chases the tiger. If something visits the mouse then it is nice. If the mouse sees the dog and the mouse visits the dog then the dog visits the mouse. If something chases the tiger then it sees the dog.
The dog is kind.
("dog" "is" "kind" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
If something sees the tiger then the tiger is red.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something chases the dog and the dog is kind then the dog is round.
((("something" "chases" "dog" "+") ("dog" "is" "kind" "+")) -> ("dog" "is" "round" "+"))
If something is round then it chases the tiger.
((("something" "is" "round" "+")) -> ("something" "chases" "tiger" "+"))
If something visits the mouse then it is nice.
((("something" "visits" "mouse" "+")) -> ("something" "is" "nice" "+"))
If the mouse sees the dog and the mouse visits the dog then the dog visits the mouse.
((("mouse" "sees" "dog" "+") ("mouse" "visits" "dog" "+")) -> ("dog" "visits" "mouse" "+"))
If something chases the tiger then it sees the dog.
((("something" "chases" "tiger" "+")) -> ("something" "sees" "dog" "+"))
The mouse is round.
True
1
proof
[(triple4)]
("mouse" "is" "round" "+")
triple4
The mouse does not chase the tiger.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule3))]
("mouse" "chases" "tiger" "-")
triple3
((triple4) -> (rule3 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The dog is round.
True
3
proof
[(((triple6 triple1) -> rule2))]
("dog" "is" "round" "+")
((triple6 triple1) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The mouse does not see the dog.
False
2
inv-proof
[(((triple3) -> rule6) OR ((((triple4) -> rule3)) -> rule6))]
("mouse" "sees" "dog" "-")
((triple3) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The dog chases the tiger.
True
4
proof
[(((((triple6 triple1) -> rule2)) -> rule3))]
("dog" "chases" "tiger" "+")
((((triple6 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog does not chase the tiger.
False
4
inv-proof
[(((((triple6 triple1) -> rule2)) -> rule3))]
("dog" "chases" "tiger" "-")
((((triple6 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog sees the dog.
True
5
proof
[(((((((triple6 triple1) -> rule2)) -> rule3)) -> rule6))]
("dog" "sees" "dog" "+")
((((((triple6 triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The dog does not see the dog.
False
5
inv-proof
[(((((((triple6 triple1) -> rule2)) -> rule3)) -> rule6))]
("dog" "sees" "dog" "-")
((((((triple6 triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The tiger does not see the dog.
Unknown
inv-rconc
[@2: The tiger sees the dog.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("tiger" "sees" "dog" "-")
The dog is nice.
Unknown
rconc
[@2: The dog is nice.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("dog" "is" "nice" "+")
The dog does not visit the mouse.
Unknown
inv-rconc
[@1: The dog visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "visits" "mouse" "-")
The tiger is nice.
Unknown
rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "nice" "+")
The mouse does not visit the tiger.
Unknown
inv-random
[@0: The mouse visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "tiger" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The dog sees the tiger.
Unknown
random
[@0: The dog sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "tiger" "+")
@0: The dog is kind.[(triple1)] The dog visits the tiger.[(triple2)] The mouse chases the tiger.[(triple3 OR ((triple4) -> rule3))] The mouse is round.[(triple4)] The mouse sees the tiger.[(triple5)] The tiger chases the dog.[(triple6)] The tiger is big.[(triple7)] @1: The dog is round.[(((triple6 triple1) -> rule2))] The mouse sees the dog.[(((triple3) -> rule6) OR ((((triple4) -> rule3)) -> rule6))] The tiger is red.[(((triple5) -> rule1))] @2: The dog chases the tiger.[(((((triple6 triple1) -> rule2)) -> rule3))] @3: The dog sees the dog.[(((((((triple6 triple1) -> rule2)) -> rule3)) -> rule6))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple3
((triple4) -> (rule3 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple5
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The dog is round.
("dog" "is" "round" "+")
((triple6 triple1) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple3) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
((triple5) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
((((triple6 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
((((((triple6 triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3