The bear is round. The cat is cold. The cat is round. The cow is cold. The cow likes the cat. The cow needs the rabbit. The rabbit is kind. The rabbit does not need the cow. The rabbit sees the bear. The rabbit does not see the cat. If something likes the cow then the cow likes the bear. If the bear likes the cat then the cat likes the cow. All cold things are green. If something sees the cat then the cat does not like the bear. If something is red then it likes the cat. If something needs the cow then the cow needs the bear. If something likes the bear then it sees the cow. If something is round then it is red. If something sees the rabbit then the rabbit is red.
The bear is round.
("bear" "is" "round" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is round.
("cat" "is" "round" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
If something likes the cow then the cow likes the bear.
((("something" "likes" "cow" "+")) -> ("cow" "likes" "bear" "+"))
If the bear likes the cat then the cat likes the cow.
((("bear" "likes" "cat" "+")) -> ("cat" "likes" "cow" "+"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something sees the cat then the cat does not like the bear.
((("something" "sees" "cat" "+")) -> ("cat" "likes" "bear" "-"))
If something is red then it likes the cat.
((("something" "is" "red" "+")) -> ("something" "likes" "cat" "+"))
If something needs the cow then the cow needs the bear.
((("something" "needs" "cow" "+")) -> ("cow" "needs" "bear" "+"))
If something likes the bear then it sees the cow.
((("something" "likes" "bear" "+")) -> ("something" "sees" "cow" "+"))
If something is round then it is red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something sees the rabbit then the rabbit is red.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
The cat is cold.
True
1
proof
[(triple2)]
("cat" "is" "cold" "+")
triple2
The rabbit needs the cow.
False
1
inv-proof
[(triple8)]
("rabbit" "needs" "cow" "+")
triple8
The cat is green.
True
2
proof
[(((triple2) -> rule3))]
("cat" "is" "green" "+")
((triple2) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple3) -> rule8))]
("cat" "is" "red" "-")
((triple3) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bear likes the cat.
True
3
proof
[(((((triple1) -> rule8)) -> rule5))]
("bear" "likes" "cat" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The cat does not like the cat.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule5))]
("cat" "likes" "cat" "-")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat likes the cow.
True
4
proof
[(((((((triple1) -> rule8)) -> rule5)) -> rule2))]
("cat" "likes" "cow" "+")
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The cat does not like the cow.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule5)) -> rule2))]
("cat" "likes" "cow" "-")
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The cow likes the bear.
True
5
proof
[(((((((((triple1) -> rule8)) -> rule5)) -> rule2)) -> rule1))]
("cow" "likes" "bear" "+")
((((((((triple1) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The cow does not like the bear.
False
5
inv-proof
[(((((((((triple1) -> rule8)) -> rule5)) -> rule2)) -> rule1))]
("cow" "likes" "bear" "-")
((((((((triple1) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The cow sees the cow.
True
6
proof
[(((((((((((triple1) -> rule8)) -> rule5)) -> rule2)) -> rule1)) -> rule7))]
("cow" "sees" "cow" "+")
((((((((((triple1) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The bear is red.
("bear" "is" "red" "+")
int5
The cow does not see the cow.
False
6
inv-proof
[(((((((((((triple1) -> rule8)) -> rule5)) -> rule2)) -> rule1)) -> rule7))]
("cow" "sees" "cow" "-")
((((((((((triple1) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The bear is red.
("bear" "is" "red" "+")
int5
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "green" "-")
The bear is green.
Unknown
rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "green" "+")
The cow does not need the bear.
Unknown
inv-rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "needs" "bear" "-")
The rabbit sees the cow.
Unknown
rconc
[@1: The rabbit sees the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "sees" "cow" "+")
The cat does not see the cow.
Unknown
inv-rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "sees" "cow" "-")
The rabbit is red.
Unknown
rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "red" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The bear sees the rabbit.
Unknown
random
[@0: The bear sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The bear is round.[(triple1)] The cat is cold.[(triple2)] The cat is round.[(triple3)] The cow is cold.[(triple4)] The cow likes the cat.[(triple5)] The cow needs the rabbit.[(triple6)] The rabbit does not need the cow.[(triple8)] The rabbit does not see the cat.[(triple10)] The rabbit is kind.[(triple7)] The rabbit sees the bear.[(triple9)] @1: The bear is red.[(((triple1) -> rule8))] The cat is green.[(((triple2) -> rule3))] The cat is red.[(((triple3) -> rule8))] The cow is green.[(((triple4) -> rule3))] @2: The bear likes the cat.[(((((triple1) -> rule8)) -> rule5))] The cat likes the cat.[(((((triple3) -> rule8)) -> rule5))] @3: The cat likes the cow.[(((((((triple1) -> rule8)) -> rule5)) -> rule2))] @4: The cow likes the bear.[(((((((((triple1) -> rule8)) -> rule5)) -> rule2)) -> rule1))] @5: The cow sees the cow.[(((((((((((triple1) -> rule8)) -> rule5)) -> rule2)) -> rule1)) -> rule7))]
The bear is round.
("bear" "is" "round" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow likes the cat.
("cow" "likes" "cat" "+")
triple5
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple6
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
triple8
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple9
The bear is red.
("bear" "is" "red" "+")
((triple1) -> (rule8 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((triple2) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((triple3) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cow is green.
("cow" "is" "green" "+")
((triple4) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The cow likes the bear.
("cow" "likes" "bear" "+")
((((((((triple1) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The bear likes the cat.
("bear" "likes" "cat" "+")
int3
The bear is red.
("bear" "is" "red" "+")
int4
The cow sees the cow.
("cow" "sees" "cow" "+")
((((((((((triple1) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The bear likes the cat.
("bear" "likes" "cat" "+")
int4
The bear is red.
("bear" "is" "red" "+")
int5