Charlie is not blue. Charlie is nice. Charlie is white. Dave is blue. Dave is rough. Fiona is blue. Fiona is nice. Gary is furry. Gary is smart. Gary is white. If someone is nice then they are quiet. Nice, white people are quiet. If Gary is nice then Gary is furry. All nice, quiet people are white. Quiet, smart people are rough. All nice, rough people are furry. If someone is smart and blue then they are furry. Smart, white people are nice.
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Nice, white people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is nice then Gary is furry.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "furry" "+"))
All nice, quiet people are white.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Quiet, smart people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All nice, rough people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and blue then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Smart, white people are nice.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Fiona is not blue.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "blue" "-")
triple6
Gary is nice.
True
3
proof
[(((triple9 triple10) -> rule8))]
("Gary" "is" "nice" "+")
((triple9 triple10) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
3
inv-proof
[(((triple9 triple10) -> rule8))]
("Gary" "is" "nice" "-")
((triple9 triple10) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
True
4
proof
[(((((triple9 triple10) -> rule8)) -> rule1) OR ((((triple9 triple10) -> rule8) triple10) -> rule2))]
("Gary" "is" "quiet" "+")
((((triple9 triple10) -> (rule8 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple9 triple10) -> (rule8 % int2)) triple10) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Fiona is not white.
False
4
inv-proof
[(((triple7 ((triple7) -> rule1)) -> rule4))]
("Fiona" "is" "white" "-")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Gary is rough.
True
6
proof
[(((((((triple9 triple10) -> rule8)) -> rule1) triple9) -> rule5) OR ((((((triple9 triple10) -> rule8) triple10) -> rule2) triple9) -> rule5))]
("Gary" "is" "rough" "+")
((((((triple9 triple10) -> (rule8 % int3))) -> (rule1 % int2)) triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple9 triple10) -> (rule8 % int3)) triple10) -> (rule2 % int2)) triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not rough.
False
6
inv-proof
[(((((((triple9 triple10) -> rule8)) -> rule1) triple9) -> rule5) OR ((((((triple9 triple10) -> rule8) triple10) -> rule2) triple9) -> rule5))]
("Gary" "is" "rough" "-")
((((((triple9 triple10) -> (rule8 % int3))) -> (rule1 % int2)) triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple9 triple10) -> (rule8 % int3)) triple10) -> (rule2 % int2)) triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "furry" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is quiet.
Unknown
rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Dave" "is" "quiet" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Charlie is nice.[(triple2)] Charlie is not blue.[(triple1)] Charlie is white.[(triple3 OR ((triple2 ((triple2) -> rule1)) -> rule4))] Dave is blue.[(triple4)] Dave is rough.[(triple5)] Fiona is blue.[(triple6)] Fiona is nice.[(triple7)] Gary is furry.[(triple8 OR ((((triple9 triple10) -> rule8)) -> rule3) OR ((((triple9 triple10) -> rule8) ((((((triple9 triple10) -> rule8)) -> rule1) triple9) -> rule5)) -> rule6) OR ((((triple9 triple10) -> rule8) ((((((triple9 triple10) -> rule8) triple10) -> rule2) triple9) -> rule5)) -> rule6))] Gary is smart.[(triple9)] Gary is white.[(triple10)] @1: Charlie is quiet.[(((triple2) -> rule1) OR ((triple2 triple3) -> rule2))] Fiona is quiet.[(((triple7) -> rule1))] Gary is nice.[(((triple9 triple10) -> rule8))] @2: Fiona is white.[(((triple7 ((triple7) -> rule1)) -> rule4))] Gary is quiet.[(((((triple9 triple10) -> rule8)) -> rule1) OR ((((triple9 triple10) -> rule8) triple10) -> rule2))] @3: Gary is rough.[(((((((triple9 triple10) -> rule8)) -> rule1) triple9) -> rule5) OR ((((((triple9 triple10) -> rule8) triple10) -> rule2) triple9) -> rule5))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple3
((triple2 ((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
((((triple9 triple10) -> (rule8 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple9 triple10) -> (rule8 % int4)) ((((((triple9 triple10) -> (rule8 % int4))) -> (rule1 % int3)) triple9) -> (rule5 % int2))) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
((((triple9 triple10) -> (rule8 % int4)) ((((((triple9 triple10) -> (rule8 % int4)) triple10) -> (rule2 % int3)) triple9) -> (rule5 % int2))) -> (rule6 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2 triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple9 triple10) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple9 triple10) -> (rule8 % int2))) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple9 triple10) -> (rule8 % int2)) triple10) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple9 triple10) -> (rule8 % int3))) -> (rule1 % int2)) triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple9 triple10) -> (rule8 % int3)) triple10) -> (rule2 % int2)) triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3