The cat is big. The cat needs the tiger. The cat sees the dog. The dog is rough. The mouse needs the tiger. The tiger is blue. The tiger sees the mouse. If the cat is blue then the cat is kind. If something is big and kind then it visits the cat. If something is round then it sees the mouse. If something is blue then it needs the dog. If something is big then it is round. If the tiger visits the dog then the tiger visits the mouse. If something is round and it sees the mouse then the mouse is big. If something sees the tiger then the tiger needs the cat.
The cat is big.
("cat" "is" "big" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog is rough.
("dog" "is" "rough" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the cat is blue then the cat is kind.
((("cat" "is" "blue" "+")) -> ("cat" "is" "kind" "+"))
If something is big and kind then it visits the cat.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "visits" "cat" "+"))
If something is round then it sees the mouse.
((("something" "is" "round" "+")) -> ("something" "sees" "mouse" "+"))
If something is blue then it needs the dog.
((("something" "is" "blue" "+")) -> ("something" "needs" "dog" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If the tiger visits the dog then the tiger visits the mouse.
((("tiger" "visits" "dog" "+")) -> ("tiger" "visits" "mouse" "+"))
If something is round and it sees the mouse then the mouse is big.
((("something" "is" "round" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something sees the tiger then the tiger needs the cat.
((("something" "sees" "tiger" "+")) -> ("tiger" "needs" "cat" "+"))
The cat sees the dog.
True
1
proof
[(triple3)]
("cat" "sees" "dog" "+")
triple3
The tiger does not see the mouse.
False
1
inv-proof
[(triple7)]
("tiger" "sees" "mouse" "-")
triple7
The cat is round.
True
2
proof
[(((triple1) -> rule5))]
("cat" "is" "round" "+")
((triple1) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger does not need the dog.
False
2
inv-proof
[(((triple6) -> rule4))]
("tiger" "needs" "dog" "-")
((triple6) -> (rule4 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The cat sees the mouse.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("cat" "sees" "mouse" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat does not see the mouse.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("cat" "sees" "mouse" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The mouse is big.
True
6
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7))]
("mouse" "is" "big" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse is not big.
False
6
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7))]
("mouse" "is" "big" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse is round.
True
7
proof
[(((((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7)) -> rule5))]
("mouse" "is" "round" "+")
((((((triple1) -> (rule5 % int4)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
The mouse is not round.
False
7
inv-proof
[(((((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7)) -> rule5))]
("mouse" "is" "round" "-")
((((((triple1) -> (rule5 % int4)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
The mouse sees the mouse.
True
8
proof
[(((((((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7)) -> rule5)) -> rule3))]
("mouse" "sees" "mouse" "+")
((((((((triple1) -> (rule5 % int5)) ((((triple1) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int4
The cat is round.
("cat" "is" "round" "+")
int5
The mouse does not see the mouse.
False
8
inv-proof
[(((((((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7)) -> rule5)) -> rule3))]
("mouse" "sees" "mouse" "-")
((((((((triple1) -> (rule5 % int5)) ((((triple1) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int4
The cat is round.
("cat" "is" "round" "+")
int5
The dog does not see the mouse.
Unknown
inv-rconc
[@2: The dog sees the mouse.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("dog" "sees" "mouse" "-")
The cat visits the cat.
Unknown
rconc
[@2: The cat visits the cat.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "visits" "cat" "+")
The mouse does not visit the cat.
Unknown
inv-rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "cat" "-")
The dog is round.
Unknown
rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "round" "+")
The tiger does not need the cat.
Unknown
inv-rconc
[@1: The tiger needs the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "needs" "cat" "-")
The tiger visits the cat.
Unknown
rconc
[@1: The tiger visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "cat" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat visits the dog.
Unknown
random
[@0: The cat visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "dog" "+")
The dog does not visit the tiger.
Unknown
inv-random
[@0: The dog visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "tiger" "-")
The dog needs the tiger.
Unknown
random
[@0: The dog needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "tiger" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The tiger needs the mouse.
Unknown
random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "+")
@0: The cat is big.[(triple1)] The cat needs the tiger.[(triple2)] The cat sees the dog.[(triple3)] The dog is rough.[(triple4)] The mouse needs the tiger.[(triple5)] The tiger is blue.[(triple6)] The tiger sees the mouse.[(triple7)] @1: The cat is round.[(((triple1) -> rule5))] The tiger needs the dog.[(((triple6) -> rule4))] @2: The cat sees the mouse.[(((((triple1) -> rule5)) -> rule3))] @3: The mouse is big.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7))] @4: The mouse is round.[(((((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7)) -> rule5))] @5: The mouse sees the mouse.[(((((((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule7)) -> rule5)) -> rule3))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple2
The cat sees the dog.
("cat" "sees" "dog" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple7
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((triple6) -> (rule4 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The mouse is round.
("mouse" "is" "round" "+")
((((((triple1) -> (rule5 % int4)) ((((triple1) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((((triple1) -> (rule5 % int5)) ((((triple1) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int4
The cat is round.
("cat" "is" "round" "+")
int5