The cat chases the dog. The cat is kind. The cat needs the dog. The cat needs the mouse. The dog is round. The dog likes the cat. The dog needs the mouse. The dog needs the tiger. The mouse chases the dog. The mouse chases the tiger. The mouse is nice. The mouse needs the dog. The mouse needs the tiger. The tiger chases the dog. The tiger is kind. The tiger needs the mouse. If someone likes the mouse and they like the tiger then they are rough. If the cat likes the dog then the cat is kind. If someone is rough then they like the mouse. If someone likes the mouse then the mouse is kind. If someone is kind and rough then they like the tiger. All nice people are rough. If the dog needs the cat then the dog is nice. If someone likes the tiger then the tiger is round.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The dog is round.
("dog" "is" "round" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If someone likes the mouse and they like the tiger then they are rough.
((("someone" "likes" "mouse" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "is" "rough" "+"))
If the cat likes the dog then the cat is kind.
((("cat" "likes" "dog" "+")) -> ("cat" "is" "kind" "+"))
If someone is rough then they like the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the mouse then the mouse is kind.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If someone is kind and rough then they like the tiger.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "likes" "tiger" "+"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If the dog needs the cat then the dog is nice.
((("dog" "needs" "cat" "+")) -> ("dog" "is" "nice" "+"))
If someone likes the tiger then the tiger is round.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "round" "+"))
The dog is round.
True
1
proof
[(triple5)]
("dog" "is" "round" "+")
triple5
The mouse is not nice.
False
1
inv-proof
[(triple11)]
("mouse" "is" "nice" "-")
triple11
The mouse is rough.
True
2
proof
[(((triple11) -> rule6))]
("mouse" "is" "rough" "+")
((triple11) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple11) -> rule6))]
("mouse" "is" "rough" "-")
((triple11) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the mouse.
True
3
proof
[(((((triple11) -> rule6)) -> rule3))]
("mouse" "likes" "mouse" "+")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not like the mouse.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule3))]
("mouse" "likes" "mouse" "-")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
True
4
proof
[(((((((triple11) -> rule6)) -> rule3)) -> rule4))]
("mouse" "is" "kind" "+")
((((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is not kind.
False
4
inv-proof
[(((((((triple11) -> rule6)) -> rule3)) -> rule4))]
("mouse" "is" "kind" "-")
((((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse likes the tiger.
True
7
proof
[(((((((((triple11) -> rule6)) -> rule3)) -> rule4) ((triple11) -> rule6)) -> rule5))]
("mouse" "likes" "tiger" "+")
((((((((triple11) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((triple11) -> (rule6 % int4))) -> (rule5 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse does not like the tiger.
False
7
inv-proof
[(((((((((triple11) -> rule6)) -> rule3)) -> rule4) ((triple11) -> rule6)) -> rule5))]
("mouse" "likes" "tiger" "-")
((((((((triple11) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((triple11) -> (rule6 % int4))) -> (rule5 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The tiger is round.
True
8
proof
[(((((((((((triple11) -> rule6)) -> rule3)) -> rule4) ((triple11) -> rule6)) -> rule5)) -> rule8))]
("tiger" "is" "round" "+")
((((((((((triple11) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule4 % int3)) ((triple11) -> (rule6 % int5))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
int5
The tiger is not round.
False
8
inv-proof
[(((((((((((triple11) -> rule6)) -> rule3)) -> rule4) ((triple11) -> rule6)) -> rule5)) -> rule8))]
("tiger" "is" "round" "-")
((((((((((triple11) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule4 % int3)) ((triple11) -> (rule6 % int5))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
int5
The dog does not like the tiger.
Unknown
inv-rconc
[@1: The dog likes the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "likes" "tiger" "-")
The cat is rough.
Unknown
rconc
[@3: The cat is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- FAIL)]]
("cat" "is" "rough" "+")
The cat does not like the mouse.
Unknown
inv-rconc
[@2: The cat likes the mouse.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("cat" "likes" "mouse" "-")
The tiger is rough.
Unknown
rconc
[@3: The tiger is rough.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- FAIL)]]
("tiger" "is" "rough" "+")
The dog is not rough.
Unknown
inv-rconc
[@2: The dog is rough.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("dog" "is" "rough" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "nice" "+")
The mouse does not chase the cat.
Unknown
inv-random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The cat does not need the tiger.
Unknown
inv-random
[@0: The cat needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "tiger" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
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 cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat chases the dog.[(triple1)] The cat is kind.[(triple2)] The cat needs the dog.[(triple3)] The cat needs the mouse.[(triple4)] The dog is round.[(triple5)] The dog likes the cat.[(triple6)] The dog needs the mouse.[(triple7)] The dog needs the tiger.[(triple8)] The mouse chases the dog.[(triple9)] The mouse chases the tiger.[(triple10)] The mouse is nice.[(triple11)] The mouse needs the dog.[(triple12)] The mouse needs the tiger.[(triple13)] The tiger chases the dog.[(triple14)] The tiger is kind.[(triple15)] The tiger needs the mouse.[(triple16)] @1: The mouse is rough.[(((triple11) -> rule6))] @2: The mouse likes the mouse.[(((((triple11) -> rule6)) -> rule3))] @3: The mouse is kind.[(((((((triple11) -> rule6)) -> rule3)) -> rule4))] @4: The mouse likes the tiger.[(((((((((triple11) -> rule6)) -> rule3)) -> rule4) ((triple11) -> rule6)) -> rule5))] @5: The tiger is round.[(((((((((((triple11) -> rule6)) -> rule3)) -> rule4) ((triple11) -> rule6)) -> rule5)) -> rule8))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog likes the cat.
("dog" "likes" "cat" "+")
triple6
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple7
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple8
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple9
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple10
The mouse is nice.
("mouse" "is" "nice" "+")
triple11
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple12
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple13
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple14
The tiger is kind.
("tiger" "is" "kind" "+")
triple15
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple16
The mouse is rough.
("mouse" "is" "rough" "+")
((triple11) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
((((((triple11) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((((((((triple11) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((triple11) -> (rule6 % int4))) -> (rule5 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
((((((((((triple11) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule4 % int3)) ((triple11) -> (rule6 % int5))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
int5