Anne is not round. Gary is rough. Harry is young. If something is red and round then it is nice. All rough things are young. If Gary is nice and Gary is rough then Gary is green. Green, young things are not red. If something is rough then it is not round. If something is young and green then it is cold. If something is rough then it is cold. If something is cold then it is green.
Anne is not round.
("Anne" "is" "round" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is red and round then it is nice.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If Gary is nice and Gary is rough then Gary is green.
((("Gary" "is" "nice" "+") ("Gary" "is" "rough" "+")) -> ("Gary" "is" "green" "+"))
Green, young things are not red.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "-"))
If something is rough then it is not round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "-"))
If something is young and green then it is cold.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Gary is not rough.
False
1
inv-proof
[(triple2)]
("Gary" "is" "rough" "-")
triple2
Gary is not round.
True
2
proof
[(((triple2) -> rule5))]
("Gary" "is" "round" "-")
((triple2) -> (rule5 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is not cold.
False
2
inv-proof
[(((triple2) -> rule7))]
("Gary" "is" "cold" "-")
((triple2) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
True
3
proof
[(((((triple2) -> rule7)) -> rule8))]
("Gary" "is" "green" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule8))]
("Gary" "is" "green" "-")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not red.
True
6
proof
[(((((((triple2) -> rule7)) -> rule8) ((triple2) -> rule2)) -> rule4))]
("Gary" "is" "red" "-")
((((((triple2) -> (rule7 % int4))) -> (rule8 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Gary is red.
False
6
inv-proof
[(((((((triple2) -> rule7)) -> rule8) ((triple2) -> rule2)) -> rule4))]
("Gary" "is" "red" "+")
((((((triple2) -> (rule7 % int4))) -> (rule8 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is cold.
Unknown
rconc
[@3: Harry is cold.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule7 <- FAIL)]]
("Harry" "is" "cold" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Anne is not round.[(triple1)] Gary is rough.[(triple2)] Harry is young.[(triple3)] @1: Gary is cold.[(((triple2) -> rule7))] Gary is not round.[(((triple2) -> rule5))] Gary is young.[(((triple2) -> rule2))] @2: Gary is green.[(((((triple2) -> rule7)) -> rule8))] @3: Gary is not red.[(((((((triple2) -> rule7)) -> rule8) ((triple2) -> rule2)) -> rule4))]
Anne is not round.
("Anne" "is" "round" "-")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
((triple2) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
((triple2) -> (rule5 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is not red.
("Gary" "is" "red" "-")
((((((triple2) -> (rule7 % int4))) -> (rule8 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
int4