The dog visits the rabbit. The rabbit eats the dog. If something chases the dog then it chases the rabbit. If something eats the rabbit then the rabbit chases the dog. If something eats the dog then the dog eats the rabbit. If something chases the dog and it visits the rabbit then the dog chases the rabbit. If something is cold then it chases the dog. If something visits the rabbit then it visits the dog. If something chases the dog then the dog visits the rabbit. If something visits the dog then it is cold.
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
If something chases the dog then it chases the rabbit.
((("something" "chases" "dog" "+")) -> ("something" "chases" "rabbit" "+"))
If something eats the rabbit then the rabbit chases the dog.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
If something eats the dog then the dog eats the rabbit.
((("something" "eats" "dog" "+")) -> ("dog" "eats" "rabbit" "+"))
If something chases the dog and it visits the rabbit then the dog chases the rabbit.
((("something" "chases" "dog" "+") ("something" "visits" "rabbit" "+")) -> ("dog" "chases" "rabbit" "+"))
If something is cold then it chases the dog.
((("something" "is" "cold" "+")) -> ("something" "chases" "dog" "+"))
If something visits the rabbit then it visits the dog.
((("something" "visits" "rabbit" "+")) -> ("something" "visits" "dog" "+"))
If something chases the dog then the dog visits the rabbit.
((("something" "chases" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If something visits the dog then it is cold.
((("something" "visits" "dog" "+")) -> ("something" "is" "cold" "+"))
The dog visits the rabbit.
True
1
proof
[(triple1 OR ((((((triple2) -> rule3)) -> rule2)) -> rule7))]
("dog" "visits" "rabbit" "+")
triple1
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog does not visit the rabbit.
False
1
inv-proof
[(triple1 OR ((((((triple2) -> rule3)) -> rule2)) -> rule7))]
("dog" "visits" "rabbit" "-")
triple1
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog visits the dog.
True
2
proof
[(((triple1) -> rule6) OR ((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6))]
("dog" "visits" "dog" "+")
((triple1) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((((((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int4
The dog does not eat the rabbit.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "eats" "rabbit" "-")
((triple2) -> (rule3 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit chases the dog.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("rabbit" "chases" "dog" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog is not cold.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule8) OR ((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6)) -> rule8))]
("dog" "is" "cold" "-")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
((((((((((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int3
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int4
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int5
The rabbit chases the rabbit.
True
4
proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule1))]
("rabbit" "chases" "rabbit" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The rabbit does not chase the rabbit.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule2)) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The rabbit is not cold.
Unknown
inv-rconc
[@2: The rabbit is cold.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit visits the dog.
Unknown
rconc
[@1: The rabbit visits the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "dog" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The dog visits the rabbit.[(triple1 OR ((((((triple2) -> rule3)) -> rule2)) -> rule7))] The rabbit eats the dog.[(triple2)] @1: The dog eats the rabbit.[(((triple2) -> rule3))] The dog visits the dog.[(((triple1) -> rule6) OR ((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6))] @2: The dog is cold.[(((((triple1) -> rule6)) -> rule8) OR ((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6)) -> rule8))] The rabbit chases the dog.[(((((triple2) -> rule3)) -> rule2))] @3: The dog chases the dog.[(((((((triple1) -> rule6)) -> rule8)) -> rule5) OR ((((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6)) -> rule8)) -> rule5))] The rabbit chases the rabbit.[(((((((triple2) -> rule3)) -> rule2)) -> rule1))] @4: The dog chases the rabbit.[(((((((((triple1) -> rule6)) -> rule8)) -> rule5)) -> rule1) OR ((((((((triple1) -> rule6)) -> rule8)) -> rule5) triple1) -> rule4) OR ((((((((triple1) -> rule6)) -> rule8)) -> rule5) ((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule4) OR ((((((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6)) -> rule8)) -> rule5)) -> rule1) OR ((((((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6)) -> rule8)) -> rule5) triple1) -> rule4) OR ((((((((((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule6)) -> rule8)) -> rule5) ((((((triple2) -> rule3)) -> rule2)) -> rule7)) -> rule4))]
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple1
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
((triple2) -> (rule3 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple1) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
((((((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int4
The dog is cold.
("dog" "is" "cold" "+")
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
((((((((((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int3
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int4
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
((((((((((((triple2) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int4
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int5
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int6
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
int4
((((((((triple1) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
int4
((((((((triple1) -> (rule6 % int7))) -> (rule8 % int6))) -> (rule5 % int5)) ((((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int4
The dog chases the dog.
("dog" "chases" "dog" "+")
int5
The dog is cold.
("dog" "is" "cold" "+")
int6
The dog visits the dog.
("dog" "visits" "dog" "+")
int7
((((((((((((((triple2) -> (rule3 % int7))) -> (rule2 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
int4
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int6
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int7
((((((((((((((triple2) -> (rule3 % int7))) -> (rule2 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
int4
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int6
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int7
((((((((((((((triple2) -> (rule3 % int7))) -> (rule2 % int6))) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule5 % int2)) ((((((triple2) -> (rule3 % int7))) -> (rule2 % int6))) -> (rule7 % int5))) -> (rule4 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog visits the dog.
("dog" "visits" "dog" "+")
int4
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int6
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int7