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