Anne is smart. Gary is young. Harry is not round. If something is blue then it is red. If something is young then it is green. Green things are blue.
Anne is smart.
("Anne" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not round.
("Harry" "is" "round" "-")
If something is blue then it is red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Gary is not young.
False
1
inv-proof
[(triple2)]
("Gary" "is" "young" "-")
triple2
Gary is green.
True
2
proof
[(((triple2) -> rule2))]
("Gary" "is" "green" "+")
((triple2) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Gary" "is" "green" "-")
((triple2) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Gary" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Gary" "is" "blue" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
True
4
proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Gary" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is not red.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Gary" "is" "red" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Harry is red.
Unknown
rconc
[@3: Harry is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Harry" "is" "red" "+")
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "blue" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "green" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is smart.[(triple1)] Gary is young.[(triple2)] Harry is not round.[(triple3)] @1: Gary is green.[(((triple2) -> rule2))] @2: Gary is blue.[(((((triple2) -> rule2)) -> rule3))] @3: Gary is red.[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Gary is young.
("Gary" "is" "young" "+")
triple2
Harry is not round.
("Harry" "is" "round" "-")
triple3
Gary is green.
("Gary" "is" "green" "+")
((triple2) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3