The cat visits the rabbit. The cat visits the tiger. The cow is green. The cow is nice. The cow is rough. The cow needs the rabbit. The rabbit is rough. The tiger is green. The tiger is nice. The tiger is round. The tiger visits the cow. If someone visits the rabbit then the rabbit needs the tiger. If someone visits the cat then they need the rabbit. If someone is nice then they chase the rabbit. If someone is kind then they need the rabbit. If someone is round and they chase the rabbit then the rabbit is green. If someone visits the rabbit and the rabbit is green then they are kind. If someone needs the rabbit then they are round. If someone is rough then they need the cow. If someone visits the rabbit and the rabbit visits the cat then the rabbit chases the cat.
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If someone visits the rabbit then the rabbit needs the tiger.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "needs" "tiger" "+"))
If someone visits the cat then they need the rabbit.
((("someone" "visits" "cat" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone is nice then they chase the rabbit.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone is kind then they need the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone is round and they chase the rabbit then the rabbit is green.
((("someone" "is" "round" "+") ("someone" "chases" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If someone visits the rabbit and the rabbit is green then they are kind.
((("someone" "visits" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the rabbit then they are round.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they need the cow.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "cow" "+"))
If someone visits the rabbit and the rabbit visits the cat then the rabbit chases the cat.
((("someone" "visits" "rabbit" "+") ("rabbit" "visits" "cat" "+")) -> ("rabbit" "chases" "cat" "+"))
The cow is green.
True
1
proof
[(triple3)]
("cow" "is" "green" "+")
triple3
The cow does not need the rabbit.
False
1
inv-proof
[(triple6)]
("cow" "needs" "rabbit" "-")
triple6
The cow is round.
True
2
proof
[(((triple6) -> rule7))]
("cow" "is" "round" "+")
((triple6) -> (rule7 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The tiger does not chase the rabbit.
False
2
inv-proof
[(((triple9) -> rule3))]
("tiger" "chases" "rabbit" "-")
((triple9) -> (rule3 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The rabbit is green.
True
4
proof
[(((triple10 ((triple9) -> rule3)) -> rule5) OR ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5))]
("rabbit" "is" "green" "+")
((triple10 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
((((triple6) -> (rule7 % int3)) ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The rabbit is not green.
False
4
inv-proof
[(((triple10 ((triple9) -> rule3)) -> rule5) OR ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5))]
("rabbit" "is" "green" "-")
((triple10 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
((((triple6) -> (rule7 % int3)) ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cat is kind.
True
6
proof
[(((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6) OR ((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6))]
("cat" "is" "kind" "+")
((triple1 ((triple10 ((triple9) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int3
((triple1 ((((triple6) -> (rule7 % int4)) ((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cat is not kind.
False
6
inv-proof
[(((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6) OR ((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6))]
("cat" "is" "kind" "-")
((triple1 ((triple10 ((triple9) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int3
((triple1 ((((triple6) -> (rule7 % int4)) ((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cat needs the rabbit.
True
7
proof
[(((((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6)) -> rule4) OR ((((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6)) -> rule4))]
("cat" "needs" "rabbit" "+")
((((triple1 ((triple10 ((triple9) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int4
((((triple1 ((((triple6) -> (rule7 % int5)) ((triple4) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int4
The cow is round.
("cow" "is" "round" "+")
int5
The cat does not need the rabbit.
False
7
inv-proof
[(((((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6)) -> rule4) OR ((((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6)) -> rule4))]
("cat" "needs" "rabbit" "-")
((((triple1 ((triple10 ((triple9) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int4
((((triple1 ((((triple6) -> (rule7 % int5)) ((triple4) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int4
The cow is round.
("cow" "is" "round" "+")
int5
The cat is round.
True
8
proof
[(((((((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6)) -> rule4)) -> rule7) OR ((((((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6)) -> rule4)) -> rule7))]
("cat" "is" "round" "+")
((((((triple1 ((triple10 ((triple9) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int5
((((((triple1 ((((triple6) -> (rule7 % int6)) ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int5
The cow is round.
("cow" "is" "round" "+")
int6
The cat is not round.
False
8
inv-proof
[(((((((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6)) -> rule4)) -> rule7) OR ((((((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6)) -> rule4)) -> rule7))]
("cat" "is" "round" "-")
((((((triple1 ((triple10 ((triple9) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int5
((((((triple1 ((((triple6) -> (rule7 % int6)) ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int5
The cow is round.
("cow" "is" "round" "+")
int6
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@2: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit is not round.
Unknown
inv-rconc
[@3: The rabbit is round.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule6 <- FAIL)]]
("rabbit" "is" "round" "-")
The tiger needs the cow.
Unknown
rconc
[@1: The tiger needs the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "needs" "cow" "+")
The cat does not chase the rabbit.
Unknown
inv-rconc
[@1: The cat chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "rabbit" "-")
The tiger needs the rabbit.
Unknown
rconc
[@2: The tiger needs the rabbit.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("tiger" "needs" "rabbit" "+")
The tiger does not need the cat.
Unknown
inv-random
[@0: The tiger needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cat" "-")
The tiger visits the rabbit.
Unknown
random
[@0: The tiger visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "rabbit" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cow does not chase the cat.
Unknown
inv-random
[@0: The cow chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat visits the rabbit.[(triple1)] The cat visits the tiger.[(triple2)] The cow is green.[(triple3)] The cow is nice.[(triple4)] The cow is rough.[(triple5)] The cow needs the rabbit.[(triple6)] The rabbit is rough.[(triple7)] The tiger is green.[(triple8)] The tiger is nice.[(triple9)] The tiger is round.[(triple10)] The tiger visits the cow.[(triple11)] @1: The cow chases the rabbit.[(((triple4) -> rule3))] The cow is round.[(((triple6) -> rule7))] The cow needs the cow.[(((triple5) -> rule8))] The rabbit needs the cow.[(((triple7) -> rule8))] The rabbit needs the tiger.[(((triple1) -> rule1))] The tiger chases the rabbit.[(((triple9) -> rule3))] @2: The rabbit is green.[(((triple10 ((triple9) -> rule3)) -> rule5) OR ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5))] @3: The cat is kind.[(((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6) OR ((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6))] @4: The cat needs the rabbit.[(((((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6)) -> rule4) OR ((((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6)) -> rule4))] @5: The cat is round.[(((((((triple1 ((triple10 ((triple9) -> rule3)) -> rule5)) -> rule6)) -> rule4)) -> rule7) OR ((((((triple1 ((((triple6) -> rule7) ((triple4) -> rule3)) -> rule5)) -> rule6)) -> rule4)) -> rule7))]
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is rough.
("cow" "is" "rough" "+")
triple5
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple6
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple11
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((triple4) -> (rule3 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((triple6) -> (rule7 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple5) -> (rule8 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((triple7) -> (rule8 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
((triple1) -> (rule1 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple9) -> (rule3 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple10 ((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
((((triple6) -> (rule7 % int3)) ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The cow is round.
("cow" "is" "round" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
((triple1 ((triple10 ((triple9) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int3
((triple1 ((((triple6) -> (rule7 % int4)) ((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int3
The cow is round.
("cow" "is" "round" "+")
int4
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
((((triple1 ((triple10 ((triple9) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int4
((((triple1 ((((triple6) -> (rule7 % int5)) ((triple4) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int4
The cow is round.
("cow" "is" "round" "+")
int5
The cat is round.
("cat" "is" "round" "+")
((((((triple1 ((triple10 ((triple9) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int5
((((((triple1 ((((triple6) -> (rule7 % int6)) ((triple4) -> (rule3 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int5
The cow is round.
("cow" "is" "round" "+")
int6