Anne is cold. Anne is red. Anne is young. Dave is cold. Dave is red. Dave is not round. Erin is red. Erin is white. Gary is blue. Gary is not cold. Gary is red. Gary is not white. If someone is cold then they are young. All red, round people are young. If Erin is not round then Erin is cold. Round people are not red. All young people are blue. All green people are white.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is red.
("Gary" "is" "red" "+")
Gary is not white.
("Gary" "is" "white" "-")
If someone is cold then they are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All red, round people are young.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If Erin is not round then Erin is cold.
((("Erin" "is" "round" "~")) -> ("Erin" "is" "cold" "+"))
Round people are not red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "-"))
All young people are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Dave is cold.
True
1
proof
[(triple4)]
("Dave" "is" "cold" "+")
triple4
Anne is not red.
False
1
inv-proof
[(triple2)]
("Anne" "is" "red" "-")
triple2
Anne is blue.
True
2
proof
[(((triple3) -> rule5) OR ((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is not young.
False
2
inv-proof
[(((triple4) -> rule1))]
("Dave" "is" "young" "-")
((triple4) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("Dave" "is" "blue" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule5))]
("Dave" "is" "blue" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "white" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "cold" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Anne is young.[(triple3 OR ((triple1) -> rule1))] Dave is cold.[(triple4)] Dave is not round.[(triple6)] Dave is red.[(triple5)] Erin is red.[(triple7)] Erin is white.[(triple8)] Gary is blue.[(triple9)] Gary is not cold.[(triple10)] Gary is not white.[(triple12)] Gary is red.[(triple11)] @1: Anne is blue.[(((triple3) -> rule5) OR ((((triple1) -> rule1)) -> rule5))] Dave is young.[(((triple4) -> rule1))] @2: Dave is blue.[(((((triple4) -> rule1)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is not round.
("Dave" "is" "round" "-")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is not cold.
("Gary" "is" "cold" "-")
triple10
Gary is not white.
("Gary" "is" "white" "-")
triple12
Gary is red.
("Gary" "is" "red" "+")
triple11
Anne is blue.
("Anne" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple4) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2