The cat chases the dog. The cat is big. The cat sees the dog. The dog chases the tiger. The dog is kind. The dog needs the cat. The dog sees the cat. The dog sees the tiger. The tiger chases the cat. The tiger is big. The tiger needs the dog. The tiger sees the dog. If the dog is big then the dog sees the tiger. If something is round and it sees the tiger then it sees the dog. If the dog chases the cat and the cat chases the dog then the dog needs the tiger. If the tiger needs the cat and the cat needs the dog then the dog chases the cat. If something chases the tiger then the tiger needs the cat. If something needs the tiger and it chases the cat then it sees the cat. If something chases the cat then the cat needs the dog. If something is round and it sees the tiger then the tiger needs the cat.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is big.
("cat" "is" "big" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If the dog is big then the dog sees the tiger.
((("dog" "is" "big" "+")) -> ("dog" "sees" "tiger" "+"))
If something is round and it sees the tiger then it sees the dog.
((("something" "is" "round" "+") ("something" "sees" "tiger" "+")) -> ("something" "sees" "dog" "+"))
If the dog chases the cat and the cat chases the dog then the dog needs the tiger.
((("dog" "chases" "cat" "+") ("cat" "chases" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If the tiger needs the cat and the cat needs the dog then the dog chases the cat.
((("tiger" "needs" "cat" "+") ("cat" "needs" "dog" "+")) -> ("dog" "chases" "cat" "+"))
If something chases the tiger then the tiger needs the cat.
((("something" "chases" "tiger" "+")) -> ("tiger" "needs" "cat" "+"))
If something needs the tiger and it chases the cat then it sees the cat.
((("something" "needs" "tiger" "+") ("something" "chases" "cat" "+")) -> ("something" "sees" "cat" "+"))
If something chases the cat then the cat needs the dog.
((("something" "chases" "cat" "+")) -> ("cat" "needs" "dog" "+"))
If something is round and it sees the tiger then the tiger needs the cat.
((("something" "is" "round" "+") ("something" "sees" "tiger" "+")) -> ("tiger" "needs" "cat" "+"))
The dog sees the cat.
True
1
proof
[(triple7 OR ((((((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4) triple1) -> rule3) ((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4)) -> rule6))]
("dog" "sees" "cat" "+")
triple7
((((((((triple4) -> (rule5 % int5)) ((triple9) -> (rule7 % int4))) -> (rule4 % int3)) triple1) -> (rule3 % int2)) ((((triple4) -> (rule5 % int5)) ((triple9) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The dog chases the cat.
("dog" "chases" "cat" "+")
int3
The cat needs the dog.
("cat" "needs" "dog" "+")
int4
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int5
The tiger does not need the dog.
False
1
inv-proof
[(triple11)]
("tiger" "needs" "dog" "-")
triple11
The tiger needs the cat.
True
2
proof
[(((triple4) -> rule5))]
("tiger" "needs" "cat" "+")
((triple4) -> (rule5 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The cat does not need the dog.
False
2
inv-proof
[(((triple9) -> rule7))]
("cat" "needs" "dog" "-")
((triple9) -> (rule7 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The dog chases the cat.
True
5
proof
[(((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4))]
("dog" "chases" "cat" "+")
((((triple4) -> (rule5 % int3)) ((triple9) -> (rule7 % int2))) -> (rule4 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The dog does not chase the cat.
False
5
inv-proof
[(((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4))]
("dog" "chases" "cat" "-")
((((triple4) -> (rule5 % int3)) ((triple9) -> (rule7 % int2))) -> (rule4 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The dog needs the tiger.
True
7
proof
[(((((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4) triple1) -> rule3))]
("dog" "needs" "tiger" "+")
((((((triple4) -> (rule5 % int4)) ((triple9) -> (rule7 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
int2
The cat needs the dog.
("cat" "needs" "dog" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4
The dog does not need the tiger.
False
7
inv-proof
[(((((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4) triple1) -> rule3))]
("dog" "needs" "tiger" "-")
((((((triple4) -> (rule5 % int4)) ((triple9) -> (rule7 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
int2
The cat needs the dog.
("cat" "needs" "dog" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "dog" "+")
The tiger does not see the cat.
Unknown
inv-rconc
[@1: The tiger sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "sees" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "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 need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger chases the dog.
Unknown
random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "+")
@0: The cat chases the dog.[(triple1)] The cat is big.[(triple2)] The cat sees the dog.[(triple3)] The dog chases the tiger.[(triple4)] The dog is kind.[(triple5)] The dog needs the cat.[(triple6)] The dog sees the cat.[(triple7 OR ((((((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4) triple1) -> rule3) ((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4)) -> rule6))] The dog sees the tiger.[(triple8)] The tiger chases the cat.[(triple9)] The tiger is big.[(triple10)] The tiger needs the dog.[(triple11)] The tiger sees the dog.[(triple12)] @1: The cat needs the dog.[(((triple9) -> rule7))] The tiger needs the cat.[(((triple4) -> rule5))] @2: The dog chases the cat.[(((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4))] @3: The dog needs the tiger.[(((((((triple4) -> rule5) ((triple9) -> rule7)) -> rule4) triple1) -> rule3))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat sees the dog.
("cat" "sees" "dog" "+")
triple3
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog needs the cat.
("dog" "needs" "cat" "+")
triple6
The dog sees the cat.
("dog" "sees" "cat" "+")
triple7
((((((((triple4) -> (rule5 % int5)) ((triple9) -> (rule7 % int4))) -> (rule4 % int3)) triple1) -> (rule3 % int2)) ((((triple4) -> (rule5 % int5)) ((triple9) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int2
The dog chases the cat.
("dog" "chases" "cat" "+")
int3
The cat needs the dog.
("cat" "needs" "dog" "+")
int4
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int5
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple8
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple11
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple12
The cat needs the dog.
("cat" "needs" "dog" "+")
((triple9) -> (rule7 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((triple4) -> (rule5 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
((((triple4) -> (rule5 % int3)) ((triple9) -> (rule7 % int2))) -> (rule4 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
((((((triple4) -> (rule5 % int4)) ((triple9) -> (rule7 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
int2
The cat needs the dog.
("cat" "needs" "dog" "+")
int3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int4