Charlie is rough. Charlie is not round. Charlie is white. Charlie is not young. Erin is red. Erin is round. Fiona is cold. If Charlie is not cold then Charlie is green. Cold people are red. If someone is cold and not green then they are round. If someone is young then they are not round. If someone is cold and red then they are white. If someone is cold and not round then they are white. If someone is young and not cold then they are rough. If someone is white then they are rough.
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
If Charlie is not cold then Charlie is green.
((("Charlie" "is" "cold" "~")) -> ("Charlie" "is" "green" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and not green then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "round" "+"))
If someone is young then they are not round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "-"))
If someone is cold and red then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is cold and not round then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "white" "+"))
If someone is young and not cold then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Erin is round.
True
1
proof
[(triple6)]
("Erin" "is" "round" "+")
triple6
Fiona is not cold.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "cold" "-")
triple7
Fiona is red.
True
2
proof
[(((triple7) -> rule2))]
("Fiona" "is" "red" "+")
((triple7) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple7) -> rule2))]
("Fiona" "is" "red" "-")
((triple7) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
True
4
proof
[(((triple7 ((triple7) -> rule2)) -> rule5))]
("Fiona" "is" "white" "+")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not white.
False
4
inv-proof
[(((triple7 ((triple7) -> rule2)) -> rule5))]
("Fiona" "is" "white" "-")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
True
5
proof
[(((((triple7 ((triple7) -> rule2)) -> rule5)) -> rule8))]
("Fiona" "is" "rough" "+")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is not rough.
False
5
inv-proof
[(((((triple7 ((triple7) -> rule2)) -> rule5)) -> rule8))]
("Fiona" "is" "rough" "-")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "white" "+")
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Erin is rough.
Unknown
rconc
[@2: Erin is rough.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Erin" "is" "rough" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is not round.[(triple2)] Charlie is not young.[(triple4)] Charlie is rough.[(triple1 OR ((triple3) -> rule8))] Charlie is white.[(triple3)] Erin is red.[(triple5)] Erin is round.[(triple6)] Fiona is cold.[(triple7)] @1: Fiona is red.[(((triple7) -> rule2))] @2: Fiona is white.[(((triple7 ((triple7) -> rule2)) -> rule5))] @3: Fiona is rough.[(((((triple7 ((triple7) -> rule2)) -> rule5)) -> rule8))]
Charlie is not round.
("Charlie" "is" "round" "-")
triple2
Charlie is not young.
("Charlie" "is" "young" "-")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
((triple3) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
((triple7) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple7 ((triple7) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3