Dave is young. Erin is young. Gary is cold. Blue people are green. All blue, cold people are green. All cold people are blue. If Erin is not smart then Erin is rough. If someone is young and not cold then they are rough. If someone is young and not blue then they are rough.
Dave is young.
("Dave" "is" "young" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
All blue, cold people are green.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Erin is not smart then Erin is rough.
((("Erin" "is" "smart" "~")) -> ("Erin" "is" "rough" "+"))
If someone is young and not cold then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "+"))
If someone is young and not blue then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "rough" "+"))
Gary is cold.
True
1
proof
[(triple3)]
("Gary" "is" "cold" "+")
triple3
Gary is not cold.
False
1
inv-proof
[(triple3)]
("Gary" "is" "cold" "-")
triple3
Gary is blue.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
True
3
proof
[(((((triple3) -> rule3)) -> rule1) OR ((((triple3) -> rule3) triple3) -> rule2))]
("Gary" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1) OR ((((triple3) -> rule3) triple3) -> rule2))]
("Gary" "is" "green" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "rough" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Dave is young.[(triple1)] Erin is young.[(triple2)] Gary is cold.[(triple3)] @1: Gary is blue.[(((triple3) -> rule3))] @2: Gary is green.[(((((triple3) -> rule3)) -> rule1) OR ((((triple3) -> rule3) triple3) -> rule2))]
Dave is young.
("Dave" "is" "young" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
((triple3) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2