Charlie is cold. Charlie is green. Dave is blue. Dave is kind. Dave is young. Erin is blue. Fiona is rough. If something is blue and rough then it is cold. Young things are rough.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If something is blue and rough then it is cold.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Fiona is rough.
True
1
proof
[(triple7)]
("Fiona" "is" "rough" "+")
triple7
Dave is not young.
False
1
inv-proof
[(triple5)]
("Dave" "is" "young" "-")
triple5
Dave is rough.
True
2
proof
[(((triple5) -> rule2))]
("Dave" "is" "rough" "+")
((triple5) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple5) -> rule2))]
("Dave" "is" "rough" "-")
((triple5) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
True
4
proof
[(((triple3 ((triple5) -> rule2)) -> rule1))]
("Dave" "is" "cold" "+")
((triple3 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not cold.
False
4
inv-proof
[(((triple3 ((triple5) -> rule2)) -> rule1))]
("Dave" "is" "cold" "-")
((triple3 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2)] Dave is blue.[(triple3)] Dave is kind.[(triple4)] Dave is young.[(triple5)] Erin is blue.[(triple6)] Fiona is rough.[(triple7)] @1: Dave is rough.[(((triple5) -> rule2))] @2: Dave is cold.[(((triple3 ((triple5) -> rule2)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
((triple5) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple3 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2