Anne is big. Anne is not round. Charlie is big. Charlie is furry. Charlie is young. Dave is green. Gary is young. All green people are young. If someone is young then they are green. Rough people are green. If someone is green then they are cold. If someone is rough and not green then they are not round. All green people are not round.
Anne is big.
("Anne" "is" "big" "+")
Anne is not round.
("Anne" "is" "round" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Gary is young.
("Gary" "is" "young" "+")
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough and not green then they are not round.
((("someone" "is" "rough" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "round" "-"))
All green people are not round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "-"))
Anne is not round.
True
1
proof
[(triple2)]
("Anne" "is" "round" "-")
triple2
Dave is not green.
False
1
inv-proof
[(triple6)]
("Dave" "is" "green" "-")
triple6
Dave is not round.
True
2
proof
[(((triple6) -> rule6))]
("Dave" "is" "round" "-")
((triple6) -> (rule6 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is round.
False
2
inv-proof
[(((triple6) -> rule6))]
("Dave" "is" "round" "+")
((triple6) -> (rule6 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Charlie is not round.
True
3
proof
[(((((triple5) -> rule2)) -> rule6))]
("Charlie" "is" "round" "-")
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Gary is round.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule6))]
("Gary" "is" "round" "+")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Anne is not young.
Unknown
inv-rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is cold.
Unknown
rconc
[@4: Anne is cold.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- rule3 <- FAIL)]]
("Anne" "is" "cold" "+")
Anne is not green.
Unknown
inv-rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is not round.[(triple2)] Charlie is big.[(triple3)] Charlie is furry.[(triple4)] Charlie is young.[(triple5)] Dave is green.[(triple6)] Gary is young.[(triple7)] @1: Charlie is green.[(((triple5) -> rule2))] Dave is cold.[(((triple6) -> rule4))] Dave is not round.[(((triple6) -> rule6))] Dave is young.[(((triple6) -> rule1))] Gary is green.[(((triple7) -> rule2))] @2: Charlie is cold.[(((((triple5) -> rule2)) -> rule4))] Charlie is not round.[(((((triple5) -> rule2)) -> rule6))] Gary is cold.[(((((triple7) -> rule2)) -> rule4))] Gary is not round.[(((((triple7) -> rule2)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is not round.
("Anne" "is" "round" "-")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is green.
("Dave" "is" "green" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple5) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple6) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not round.
("Dave" "is" "round" "-")
((triple6) -> (rule6 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple6) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not round.
("Charlie" "is" "round" "-")
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2