The cow is cold. The cow is round. The cow likes the dog. The dog eats the cow. The dog is cold. The dog is young. The dog does not like the cow. If something eats the dog and it is round then it sees the dog. If something likes the cow and the cow is cold then it is big. If something sees the cow then it is big. If the dog is big then the dog sees the cow. If something likes the dog and it is young then the dog does not see the cow. If something sees the dog then the dog is not round. If something likes the dog and the dog is young then it eats the dog. If something likes the dog and it is not young then it sees the cow.
The cow is cold.
("cow" "is" "cold" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is young.
("dog" "is" "young" "+")
The dog does not like the cow.
("dog" "likes" "cow" "-")
If something eats the dog and it is round then it sees the dog.
((("something" "eats" "dog" "+") ("something" "is" "round" "+")) -> ("something" "sees" "dog" "+"))
If something likes the cow and the cow is cold then it is big.
((("something" "likes" "cow" "+") ("cow" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something sees the cow then it is big.
((("something" "sees" "cow" "+")) -> ("something" "is" "big" "+"))
If the dog is big then the dog sees the cow.
((("dog" "is" "big" "+")) -> ("dog" "sees" "cow" "+"))
If something likes the dog and it is young then the dog does not see the cow.
((("something" "likes" "dog" "+") ("something" "is" "young" "+")) -> ("dog" "sees" "cow" "-"))
If something sees the dog then the dog is not round.
((("something" "sees" "dog" "+")) -> ("dog" "is" "round" "-"))
If something likes the dog and the dog is young then it eats the dog.
((("something" "likes" "dog" "+") ("dog" "is" "young" "+")) -> ("something" "eats" "dog" "+"))
If something likes the dog and it is not young then it sees the cow.
((("something" "likes" "dog" "+") ("something" "is" "young" "~")) -> ("something" "sees" "cow" "+"))
The dog does not like the cow.
True
1
proof
[(triple7)]
("dog" "likes" "cow" "-")
triple7
The cow is not cold.
False
1
inv-proof
[(triple1)]
("cow" "is" "cold" "-")
triple1
The cow eats the dog.
True
3
proof
[(((triple3 triple6) -> rule7))]
("cow" "eats" "dog" "+")
((triple3 triple6) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow does not eat the dog.
False
3
inv-proof
[(((triple3 triple6) -> rule7))]
("cow" "eats" "dog" "-")
((triple3 triple6) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow sees the dog.
True
5
proof
[(((((triple3 triple6) -> rule7) triple2) -> rule1))]
("cow" "sees" "dog" "+")
((((triple3 triple6) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The cow does not see the dog.
False
5
inv-proof
[(((((triple3 triple6) -> rule7) triple2) -> rule1))]
("cow" "sees" "dog" "-")
((((triple3 triple6) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog is not round.
True
6
proof
[(((((((triple3 triple6) -> rule7) triple2) -> rule1)) -> rule6))]
("dog" "is" "round" "-")
((((((triple3 triple6) -> (rule7 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
int3
The dog is round.
False
6
inv-proof
[(((((((triple3 triple6) -> rule7) triple2) -> rule1)) -> rule6))]
("dog" "is" "round" "+")
((((((triple3 triple6) -> (rule7 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
int3
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "eats" "dog" "-")
The dog is big.
Unknown
rconc
[@3: The dog is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- FAIL)]]
("dog" "is" "big" "+")
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "-")
The cow is big.
Unknown
rconc
[@2: The cow is big.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("cow" "is" "big" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is cold.[(triple1)] The cow is round.[(triple2)] The cow likes the dog.[(triple3)] The dog does not like the cow.[(triple7)] The dog eats the cow.[(triple4)] The dog is cold.[(triple5)] The dog is young.[(triple6)] @1: The cow eats the dog.[(((triple3 triple6) -> rule7))] @2: The cow sees the dog.[(((((triple3 triple6) -> rule7) triple2) -> rule1))] @3: The dog is not round.[(((((((triple3 triple6) -> rule7) triple2) -> rule1)) -> rule6))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple3
The dog does not like the cow.
("dog" "likes" "cow" "-")
triple7
The dog eats the cow.
("dog" "eats" "cow" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The cow eats the dog.
("cow" "eats" "dog" "+")
((triple3 triple6) -> (rule7 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
((((triple3 triple6) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog is not round.
("dog" "is" "round" "-")
((((((triple3 triple6) -> (rule7 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
The dog is not round.
("dog" "is" "round" "-")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
int3