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