Erin is green. Erin is kind. Gary is green. Gary is rough. Gary is white. Harry is not cold. Harry is kind. Red things are not rough. All cold things are green. If something is kind then it is green. If something is kind then it is red. All kind things are red. If something is cold then it is young. Rough, kind things are young. If Gary is white then Gary is rough.
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Red things are not rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "-"))
All cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Rough, kind things are young.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Gary is white then Gary is rough.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "rough" "+"))
Erin is green.
True
1
proof
[(triple1 OR ((triple2) -> rule3))]
("Erin" "is" "green" "+")
triple1
((triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is not rough.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule8))]
("Gary" "is" "rough" "-")
triple4
((triple5) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "young" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Erin is green.[(triple1 OR ((triple2) -> rule3))] Erin is kind.[(triple2)] Gary is green.[(triple3)] Gary is rough.[(triple4 OR ((triple5) -> rule8))] Gary is white.[(triple5)] Harry is kind.[(triple7)] Harry is not cold.[(triple6)] @1: Erin is red.[(((triple2) -> rule4) OR ((triple2) -> rule5))] Harry is green.[(((triple7) -> rule3))] Harry is red.[(((triple7) -> rule4) OR ((triple7) -> rule5))] @2: Erin is not rough.[(((((triple2) -> rule4)) -> rule1) OR ((((triple2) -> rule5)) -> rule1))] Harry is not rough.[(((((triple7) -> rule4)) -> rule1) OR ((((triple7) -> rule5)) -> rule1))]
Erin is green.
("Erin" "is" "green" "+")
triple1
((triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
((triple5) -> (rule8 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is not cold.
("Harry" "is" "cold" "-")
triple6
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple2) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple7) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2