Charlie is red. Erin is green. Erin is white. Fiona is red. Gary is smart. Gary is white. Gary is young. If something is young and smart then it is green. All green things are red.
Charlie is red.
("Charlie" "is" "red" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is young and smart then it is green.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Gary is white.
True
1
proof
[(triple6)]
("Gary" "is" "white" "+")
triple6
Erin is not green.
False
1
inv-proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Gary is green.
True
3
proof
[(((triple7 triple5) -> rule1))]
("Gary" "is" "green" "+")
((triple7 triple5) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "red" "-")
((triple2) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is red.
True
4
proof
[(((((triple7 triple5) -> rule1)) -> rule2))]
("Gary" "is" "red" "+")
((((triple7 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not red.
False
4
inv-proof
[(((((triple7 triple5) -> rule1)) -> rule2))]
("Gary" "is" "red" "-")
((((triple7 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not white.
Unknown
inv-random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Charlie is red.[(triple1)] Erin is green.[(triple2)] Erin is white.[(triple3)] Fiona is red.[(triple4)] Gary is smart.[(triple5)] Gary is white.[(triple6)] Gary is young.[(triple7)] @1: Erin is red.[(((triple2) -> rule2))] Gary is green.[(((triple7 triple5) -> rule1))] @2: Gary is red.[(((((triple7 triple5) -> rule1)) -> rule2))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple7 triple5) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple7 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2