The cat is cold. The cat is kind. The cat sees the lion. The cat visits the dog. The dog is cold. The dog is round. The dog sees the tiger. The lion chases the tiger. The lion is rough. The tiger sees the dog. The tiger sees the lion. The tiger visits the cat. If something visits the lion then it sees the tiger. All nice things are round. If something chases the tiger then it visits the dog. If something chases the dog and it visits the lion then the dog is round. If the lion is nice then the lion visits the tiger. If something sees the cat then the cat is round. If the lion is round then the lion is rough. If something visits the lion then the lion is nice. If something is round then it visits the lion.
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is rough.
("lion" "is" "rough" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something visits the lion then it sees the tiger.
((("something" "visits" "lion" "+")) -> ("something" "sees" "tiger" "+"))
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something chases the tiger then it visits the dog.
((("something" "chases" "tiger" "+")) -> ("something" "visits" "dog" "+"))
If something chases the dog and it visits the lion then the dog is round.
((("something" "chases" "dog" "+") ("something" "visits" "lion" "+")) -> ("dog" "is" "round" "+"))
If the lion is nice then the lion visits the tiger.
((("lion" "is" "nice" "+")) -> ("lion" "visits" "tiger" "+"))
If something sees the cat then the cat is round.
((("something" "sees" "cat" "+")) -> ("cat" "is" "round" "+"))
If the lion is round then the lion is rough.
((("lion" "is" "round" "+")) -> ("lion" "is" "rough" "+"))
If something visits the lion then the lion is nice.
((("something" "visits" "lion" "+")) -> ("lion" "is" "nice" "+"))
If something is round then it visits the lion.
((("something" "is" "round" "+")) -> ("something" "visits" "lion" "+"))
The tiger sees the dog.
True
1
proof
[(triple10)]
("tiger" "sees" "dog" "+")
triple10
The cat does not visit the dog.
False
1
inv-proof
[(triple4)]
("cat" "visits" "dog" "-")
triple4
The lion visits the dog.
True
2
proof
[(((triple8) -> rule3))]
("lion" "visits" "dog" "+")
((triple8) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion does not visit the dog.
False
2
inv-proof
[(((triple8) -> rule3))]
("lion" "visits" "dog" "-")
((triple8) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion is nice.
True
3
proof
[(((((triple6) -> rule9)) -> rule8))]
("lion" "is" "nice" "+")
((((triple6) -> (rule9 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The lion is not nice.
False
3
inv-proof
[(((((triple6) -> rule9)) -> rule8))]
("lion" "is" "nice" "-")
((((triple6) -> (rule9 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The lion is round.
True
4
proof
[(((((((triple6) -> rule9)) -> rule8)) -> rule2))]
("lion" "is" "round" "+")
((((((triple6) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The lion does not visit the tiger.
False
4
inv-proof
[(((((((triple6) -> rule9)) -> rule8)) -> rule5))]
("lion" "visits" "tiger" "-")
((((((triple6) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The lion visits the lion.
True
5
proof
[(((((((((triple6) -> rule9)) -> rule8)) -> rule2)) -> rule9))]
("lion" "visits" "lion" "+")
((((((((triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The dog visits the lion.
("dog" "visits" "lion" "+")
int4
The lion does not visit the lion.
False
5
inv-proof
[(((((((((triple6) -> rule9)) -> rule8)) -> rule2)) -> rule9))]
("lion" "visits" "lion" "-")
((((((((triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The dog visits the lion.
("dog" "visits" "lion" "+")
int4
The lion sees the tiger.
True
6
proof
[(((((((((((triple6) -> rule9)) -> rule8)) -> rule2)) -> rule9)) -> rule1))]
("lion" "sees" "tiger" "+")
((((((((((triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
int4
The dog visits the lion.
("dog" "visits" "lion" "+")
int5
The lion does not see the tiger.
False
6
inv-proof
[(((((((((((triple6) -> rule9)) -> rule8)) -> rule2)) -> rule9)) -> rule1))]
("lion" "sees" "tiger" "-")
((((((((((triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
int4
The dog visits the lion.
("dog" "visits" "lion" "+")
int5
The tiger does not visit the dog.
Unknown
inv-rconc
[@1: The tiger visits the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "dog" "-")
The tiger sees the tiger.
Unknown
rconc
[@3: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- rule9 <- rule2 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not visit the lion.
Unknown
inv-rconc
[@2: The tiger visits the lion.[CWA. Example of deepest failure = (rule9 <- rule2 <- FAIL)]]
("tiger" "visits" "lion" "-")
The cat visits the lion.
Unknown
rconc
[@2: The cat visits the lion.[CWA. Example of deepest failure = (rule9 <- rule2 <- FAIL)]]
("cat" "visits" "lion" "+")
The cat does not see the tiger.
Unknown
inv-rconc
[@3: The cat sees the tiger.[CWA. Example of deepest failure = (rule1 <- rule9 <- rule2 <- FAIL)]]
("cat" "sees" "tiger" "-")
The tiger is round.
Unknown
rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "round" "+")
The dog does not chase the lion.
Unknown
inv-random
[@0: The dog chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "lion" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The tiger does not chase the dog.
Unknown
inv-random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "-")
The cat chases the tiger.
Unknown
random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "+")
The lion does not chase the cat.
Unknown
inv-random
[@0: The lion chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cat" "-")
The tiger chases the cat.
Unknown
random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "+")
@0: The cat is cold.[(triple1)] The cat is kind.[(triple2)] The cat sees the lion.[(triple3)] The cat visits the dog.[(triple4)] The dog is cold.[(triple5)] The dog is round.[(triple6)] The dog sees the tiger.[(triple7 OR ((((triple6) -> rule9)) -> rule1))] The lion chases the tiger.[(triple8)] The lion is rough.[(triple9 OR ((((((((triple6) -> rule9)) -> rule8)) -> rule2)) -> rule7))] The tiger sees the dog.[(triple10)] The tiger sees the lion.[(triple11)] The tiger visits the cat.[(triple12)] @1: The dog visits the lion.[(((triple6) -> rule9))] The lion visits the dog.[(((triple8) -> rule3))] @2: The lion is nice.[(((((triple6) -> rule9)) -> rule8))] @3: The lion is round.[(((((((triple6) -> rule9)) -> rule8)) -> rule2))] The lion visits the tiger.[(((((((triple6) -> rule9)) -> rule8)) -> rule5))] @4: The lion visits the lion.[(((((((((triple6) -> rule9)) -> rule8)) -> rule2)) -> rule9))] @5: The lion sees the tiger.[(((((((((((triple6) -> rule9)) -> rule8)) -> rule2)) -> rule9)) -> rule1))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is round.
("dog" "is" "round" "+")
triple6
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple7
((((triple6) -> (rule9 % int2))) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple8
The lion is rough.
("lion" "is" "rough" "+")
triple9
((((((((triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The dog visits the lion.
("dog" "visits" "lion" "+")
int4
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple10
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple11
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple12
The dog visits the lion.
("dog" "visits" "lion" "+")
((triple6) -> (rule9 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
((triple8) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((((triple6) -> (rule9 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
((((((triple6) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((((((triple6) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The lion visits the lion.
("lion" "visits" "lion" "+")
((((((((triple6) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule9 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The dog visits the lion.
("dog" "visits" "lion" "+")
int4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((((((((triple6) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
int4
The dog visits the lion.
("dog" "visits" "lion" "+")
int5