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