Charlie is rough. Fiona is green. Gary is kind. Gary is not rough. Gary is young. Harry is blue. Harry is kind. If something is blue then it is not young. Quiet things are young. All kind things are white. White things are not rough. Rough things are quiet. If something is kind and not young then it is green.
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is blue then it is not young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "-"))
Quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
White things are not rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "-"))
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is kind and not young then it is green.
((("something" "is" "kind" "+") ("something" "is" "young" "~")) -> ("something" "is" "green" "+"))
Harry is blue.
True
1
proof
[(triple6)]
("Harry" "is" "blue" "+")
triple6
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Harry is not rough.
True
3
proof
[(((((triple7) -> rule3)) -> rule4))]
("Harry" "is" "rough" "-")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Fiona" "is" "young" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "quiet" "+")
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "green" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Charlie is rough.[(triple1)] Fiona is green.[(triple2)] Gary is kind.[(triple3)] Gary is not rough.[(triple4 OR ((((triple3) -> rule3)) -> rule4))] Gary is young.[(triple5)] Harry is blue.[(triple6)] Harry is kind.[(triple7)] @1: Charlie is quiet.[(((triple1) -> rule5))] Gary is white.[(((triple3) -> rule3))] Harry is not young.[(((triple6) -> rule1))] Harry is white.[(((triple7) -> rule3))] @2: Charlie is young.[(((((triple1) -> rule5)) -> rule2))] Harry is green.[(((triple7 ((triple6) -> rule1)) -> rule6))] Harry is not rough.[(((((triple7) -> rule3)) -> rule4))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is not rough.
("Gary" "is" "rough" "-")
triple4
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
((triple6) -> (rule1 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple7) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple7 ((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
int2
Harry is not rough.
("Harry" "is" "rough" "-")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2