Anne is cold. Bob is cold. Charlie is rough. Fiona is cold. Rough things are young. If Fiona is cold and Fiona is furry then Fiona is rough. Young things are kind.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If Fiona is cold and Fiona is furry then Fiona is rough.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "rough" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Bob is cold.
True
1
proof
[(triple2)]
("Bob" "is" "cold" "+")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Charlie is young.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "young" "+")
((triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "young" "-")
((triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not kind.
Unknown
inv-rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Bob is cold.[(triple2)] Charlie is rough.[(triple3)] Fiona is cold.[(triple4)] @1: Charlie is young.[(((triple3) -> rule1))] @2: Charlie is kind.[(((((triple3) -> rule1)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
((triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2