Charlie is round. Fiona is cold. Harry is not round. All round things are green. All furry, nice things are cold. Green things are rough.
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Harry is not round.
("Harry" "is" "round" "-")
All round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All furry, nice things are cold.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Harry is round.
False
1
inv-proof
[(triple3)]
("Harry" "is" "round" "+")
triple3
Charlie is green.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "green" "+")
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "green" "-")
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is rough.
Unknown
rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Charlie is round.[(triple1)] Fiona is cold.[(triple2)] Harry is not round.[(triple3)] @1: Charlie is green.[(((triple1) -> rule1))] @2: Charlie is rough.[(((((triple1) -> rule1)) -> rule3))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Harry is not round.
("Harry" "is" "round" "-")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2