Dave is white. Fiona is not round. Gary is nice. If someone is nice and not white then they are round. All white people are round. All blue, young people are red. All nice people are red. If someone is nice then they are young. If someone is white and round then they are nice.
Dave is white.
("Dave" "is" "white" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Gary is nice.
("Gary" "is" "nice" "+")
If someone is nice and not white then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "round" "+"))
All white people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All blue, young people are red.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is white and round then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Gary is young.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "young" "+")
((triple3) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "young" "-")
((triple3) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Dave is nice.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule6))]
("Dave" "is" "nice" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule6))]
("Dave" "is" "nice" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule4))]
("Dave" "is" "red" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not young.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule5))]
("Dave" "is" "young" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Fiona" "is" "young" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Dave is white.[(triple1)] Fiona is not round.[(triple2)] Gary is nice.[(triple3)] @1: Dave is round.[(((triple1) -> rule2))] Gary is red.[(((triple3) -> rule4))] Gary is young.[(((triple3) -> rule5))] @2: Dave is nice.[(((triple1 ((triple1) -> rule2)) -> rule6))] @3: Dave is red.[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule4))] Dave is young.[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule5))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Fiona is not round.
("Fiona" "is" "round" "-")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple3) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3