Charlie is cold. Erin is cold. Erin is quiet. Erin is rough. Fiona is red. Fiona is white. Gary is rough. If someone is white and quiet then they are red. Green people are young. All rough people are white. Green, cold people are red. If someone is cold and young then they are white. If someone is quiet then they are cold. Quiet, red people are young. Quiet people are rough.
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If someone is white and quiet then they are red.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Green, cold people are red.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and young then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
Quiet, red people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Erin is not rough.
False
1
inv-proof
[(triple4 OR ((triple3) -> rule8))]
("Erin" "is" "rough" "-")
triple4
((triple3) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "young" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is cold.[(triple1)] Erin is cold.[(triple2 OR ((triple3) -> rule6))] Erin is quiet.[(triple3)] Erin is rough.[(triple4 OR ((triple3) -> rule8))] Fiona is red.[(triple5)] Fiona is white.[(triple6)] Gary is rough.[(triple7)] @1: Erin is white.[(((triple4) -> rule3) OR ((((triple3) -> rule8)) -> rule3))] Gary is white.[(((triple7) -> rule3))] @2: Erin is red.[(((((triple4) -> rule3) triple3) -> rule1) OR ((((((triple3) -> rule8)) -> rule3) triple3) -> rule1))] @3: Erin is young.[(((triple3 ((((triple4) -> rule3) triple3) -> rule1)) -> rule7) OR ((triple3 ((((((triple3) -> rule8)) -> rule3) triple3) -> rule1)) -> rule7))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple3) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
((triple3) -> (rule8 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Erin is white.
("Erin" "is" "white" "+")
((triple4) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple7) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple4) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((triple3 ((((triple4) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((triple3 ((((((triple3) -> (rule8 % int4))) -> (rule3 % int3)) triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4