Charlie is not smart. Erin is red. Harry is red. If something is rough and not red then it is cold. If something is red then it is rough. If Harry is rough then Harry is young.
Charlie is not smart.
("Charlie" "is" "smart" "-")
Erin is red.
("Erin" "is" "red" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is rough and not red then it is cold.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "cold" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Harry is rough then Harry is young.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "young" "+"))
Harry is red.
True
1
proof
[(triple3)]
("Harry" "is" "red" "+")
triple3
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Erin is rough.
True
2
proof
[(((triple2) -> rule2))]
("Erin" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "rough" "-")
((triple2) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Harry is young.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Harry" "is" "young" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Charlie is not smart.[(triple1)] Erin is red.[(triple2)] Harry is red.[(triple3)] @1: Erin is rough.[(((triple2) -> rule2))] Harry is rough.[(((triple3) -> rule2))] @2: Harry is young.[(((((triple3) -> rule2)) -> rule3))]
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2