The dog chases the lion. The dog is rough. The dog needs the lion. The dog sees the lion. The lion chases the dog. The lion is nice. The lion is red. The lion is round. The lion does not need the dog. The lion sees the dog. If the lion sees the dog and the dog chases the lion then the dog is round. If something sees the lion then it is red. If something needs the lion and the lion chases the dog then the lion sees the dog. If something needs the dog and it sees the lion then the dog does not chase the lion. If something is nice and not rough then it chases the lion. If something needs the lion then it is nice. All nice, round things are blue. If something is rough and not red then it is not round.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion does not need the dog.
("lion" "needs" "dog" "-")
The lion sees the dog.
("lion" "sees" "dog" "+")
If the lion sees the dog and the dog chases the lion then the dog is round.
((("lion" "sees" "dog" "+") ("dog" "chases" "lion" "+")) -> ("dog" "is" "round" "+"))
If something sees the lion then it is red.
((("something" "sees" "lion" "+")) -> ("something" "is" "red" "+"))
If something needs the lion and the lion chases the dog then the lion sees the dog.
((("something" "needs" "lion" "+") ("lion" "chases" "dog" "+")) -> ("lion" "sees" "dog" "+"))
If something needs the dog and it sees the lion then the dog does not chase the lion.
((("something" "needs" "dog" "+") ("something" "sees" "lion" "+")) -> ("dog" "chases" "lion" "-"))
If something is nice and not rough then it chases the lion.
((("something" "is" "nice" "+") ("something" "is" "rough" "~")) -> ("something" "chases" "lion" "+"))
If something needs the lion then it is nice.
((("something" "needs" "lion" "+")) -> ("something" "is" "nice" "+"))
All nice, round things are blue.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is rough and not red then it is not round.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "round" "-"))
The lion is red.
True
1
proof
[(triple7)]
("lion" "is" "red" "+")
triple7
The dog does not need the lion.
False
1
inv-proof
[(triple3)]
("dog" "needs" "lion" "-")
triple3
The dog is nice.
True
2
proof
[(((triple3) -> rule6))]
("dog" "is" "nice" "+")
((triple3) -> (rule6 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The lion is not blue.
False
3
inv-proof
[(((triple6 triple8) -> rule7))]
("lion" "is" "blue" "-")
((triple6 triple8) -> (rule7 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The dog is blue.
True
6
proof
[(((((triple3) -> rule6) ((triple10 triple1) -> rule1)) -> rule7) OR ((((triple3) -> rule6) ((((triple3 triple5) -> rule3) triple1) -> rule1)) -> rule7))]
("dog" "is" "blue" "+")
((((triple3) -> (rule6 % int3)) ((triple10 triple1) -> (rule1 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
((((triple3) -> (rule6 % int4)) ((((triple3 triple5) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4
The dog is not blue.
False
6
inv-proof
[(((((triple3) -> rule6) ((triple10 triple1) -> rule1)) -> rule7) OR ((((triple3) -> rule6) ((((triple3 triple5) -> rule3) triple1) -> rule1)) -> rule7))]
("dog" "is" "blue" "-")
((((triple3) -> (rule6 % int3)) ((triple10 triple1) -> (rule1 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
((((triple3) -> (rule6 % int4)) ((((triple3 triple5) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4
The lion does not chase the lion.
Unknown
inv-rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The dog chases the lion.[(triple1)] The dog is rough.[(triple2)] The dog needs the lion.[(triple3)] The dog sees the lion.[(triple4)] The lion chases the dog.[(triple5)] The lion does not need the dog.[(triple9)] The lion is nice.[(triple6)] The lion is red.[(triple7)] The lion is round.[(triple8)] The lion sees the dog.[(triple10 OR ((triple3 triple5) -> rule3))] @1: The dog is nice.[(((triple3) -> rule6))] The dog is red.[(((triple4) -> rule2))] The dog is round.[(((triple10 triple1) -> rule1) OR ((((triple3 triple5) -> rule3) triple1) -> rule1))] The lion is blue.[(((triple6 triple8) -> rule7))] @2: The dog is blue.[(((((triple3) -> rule6) ((triple10 triple1) -> rule1)) -> rule7) OR ((((triple3) -> rule6) ((((triple3 triple5) -> rule3) triple1) -> rule1)) -> rule7))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
The dog sees the lion.
("dog" "sees" "lion" "+")
triple4
The lion chases the dog.
("lion" "chases" "dog" "+")
triple5
The lion does not need the dog.
("lion" "needs" "dog" "-")
triple9
The lion is nice.
("lion" "is" "nice" "+")
triple6
The lion is red.
("lion" "is" "red" "+")
triple7
The lion is round.
("lion" "is" "round" "+")
triple8
The lion sees the dog.
("lion" "sees" "dog" "+")
triple10
((triple3 triple5) -> (rule3 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple3) -> (rule6 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((triple4) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is round.
("dog" "is" "round" "+")
((triple10 triple1) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
((((triple3 triple5) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
((triple6 triple8) -> (rule7 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple3) -> (rule6 % int3)) ((triple10 triple1) -> (rule1 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
((((triple3) -> (rule6 % int4)) ((((triple3 triple5) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The lion sees the dog.
("lion" "sees" "dog" "+")
int3
The dog is nice.
("dog" "is" "nice" "+")
int4