The lion eats the rabbit. The lion needs the rabbit. The lion sees the rabbit. The rabbit eats the lion. The rabbit is rough. The rabbit is young. The rabbit sees the lion. If something is kind and it needs the rabbit then it is young. If something sees the lion then the lion is cold. All rough things are kind. If something sees the rabbit and it is cold then it is kind. If something sees the lion then the lion needs the rabbit. If something eats the lion then it is cold. If something eats the lion and it sees the rabbit then it needs the rabbit. If the lion is young then the lion needs the rabbit.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If something is kind and it needs the rabbit then it is young.
((("something" "is" "kind" "+") ("something" "needs" "rabbit" "+")) -> ("something" "is" "young" "+"))
If something sees the lion then the lion is cold.
((("something" "sees" "lion" "+")) -> ("lion" "is" "cold" "+"))
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something sees the rabbit and it is cold then it is kind.
((("something" "sees" "rabbit" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something sees the lion then the lion needs the rabbit.
((("something" "sees" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
If something eats the lion then it is cold.
((("something" "eats" "lion" "+")) -> ("something" "is" "cold" "+"))
If something eats the lion and it sees the rabbit then it needs the rabbit.
((("something" "eats" "lion" "+") ("something" "sees" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If the lion is young then the lion needs the rabbit.
((("lion" "is" "young" "+")) -> ("lion" "needs" "rabbit" "+"))
The rabbit is rough.
True
1
proof
[(triple5)]
("rabbit" "is" "rough" "+")
triple5
The rabbit is not rough.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "rough" "-")
triple5
The rabbit is cold.
True
2
proof
[(((triple4) -> rule6))]
("rabbit" "is" "cold" "+")
((triple4) -> (rule6 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is not cold.
False
2
inv-proof
[(((triple4) -> rule6))]
("rabbit" "is" "cold" "-")
((triple4) -> (rule6 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The lion is kind.
True
4
proof
[(((triple3 ((triple7) -> rule2)) -> rule4))]
("lion" "is" "kind" "+")
((triple3 ((triple7) -> (rule2 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is not kind.
False
4
inv-proof
[(((triple3 ((triple7) -> rule2)) -> rule4))]
("lion" "is" "kind" "-")
((triple3 ((triple7) -> (rule2 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is young.
True
6
proof
[(((((triple3 ((triple7) -> rule2)) -> rule4) triple2) -> rule1) OR ((((triple3 ((triple7) -> rule2)) -> rule4) ((triple7) -> rule5)) -> rule1))]
("lion" "is" "young" "+")
((((triple3 ((triple7) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
((((triple3 ((triple7) -> (rule2 % int4))) -> (rule4 % int3)) ((triple7) -> (rule5 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The lion is not young.
False
6
inv-proof
[(((((triple3 ((triple7) -> rule2)) -> rule4) triple2) -> rule1) OR ((((triple3 ((triple7) -> rule2)) -> rule4) ((triple7) -> rule5)) -> rule1))]
("lion" "is" "young" "-")
((((triple3 ((triple7) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
((((triple3 ((triple7) -> (rule2 % int4))) -> (rule4 % int3)) ((triple7) -> (rule5 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
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 lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion eats the rabbit.[(triple1)] The lion needs the rabbit.[(triple2 OR ((triple7) -> rule5))] The lion sees the rabbit.[(triple3)] The rabbit eats the lion.[(triple4)] The rabbit is rough.[(triple5)] The rabbit is young.[(triple6)] The rabbit sees the lion.[(triple7)] @1: The lion is cold.[(((triple7) -> rule2))] The rabbit is cold.[(((triple4) -> rule6))] The rabbit is kind.[(((triple5) -> rule3))] @2: The lion is kind.[(((triple3 ((triple7) -> rule2)) -> rule4))] @3: The lion is young.[(((((triple3 ((triple7) -> rule2)) -> rule4) triple2) -> rule1) OR ((((triple3 ((triple7) -> rule2)) -> rule4) ((triple7) -> rule5)) -> rule1))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple2
((triple7) -> (rule5 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
((triple7) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple4) -> (rule6 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple5) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple3 ((triple7) -> (rule2 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((triple3 ((triple7) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
((((triple3 ((triple7) -> (rule2 % int4))) -> (rule4 % int3)) ((triple7) -> (rule5 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4