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