Anne is furry. Bob is not green. Bob is round. Charlie is cold. Charlie is not red. Gary is cold. Gary is young. If someone is green and furry then they are cold. Smart people are young. Young people are green. If Anne is furry and Anne is red then Anne is smart. If Bob is furry then Bob is not cold. If someone is furry then they are red.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is green and furry then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If Anne is furry and Anne is red then Anne is smart.
((("Anne" "is" "furry" "+") ("Anne" "is" "red" "+")) -> ("Anne" "is" "smart" "+"))
If Bob is furry then Bob is not cold.
((("Bob" "is" "furry" "+")) -> ("Bob" "is" "cold" "-"))
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Bob is not green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "cold" "-")
triple4
Gary is green.
True
2
proof
[(((triple7) -> rule3))]
("Gary" "is" "green" "+")
((triple7) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "red" "-")
((triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule4))]
("Anne" "is" "smart" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule4))]
("Anne" "is" "smart" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
True
5
proof
[(((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not young.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2))]
("Anne" "is" "young" "-")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is green.
True
6
proof
[(((((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2)) -> rule3))]
("Anne" "is" "green" "+")
((((((triple1 ((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is not green.
False
6
inv-proof
[(((((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2)) -> rule3))]
("Anne" "is" "green" "-")
((((((triple1 ((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is cold.
True
8
proof
[(((((((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2)) -> rule3) triple1) -> rule1))]
("Anne" "is" "cold" "+")
((((((((triple1 ((triple1) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Anne is not cold.
False
8
inv-proof
[(((((((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2)) -> rule3) triple1) -> rule1))]
("Anne" "is" "cold" "-")
((((((((triple1 ((triple1) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "young" "-")
Charlie is green.
Unknown
rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Charlie" "is" "green" "+")
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is furry.[(triple1)] Bob is not green.[(triple2)] Bob is round.[(triple3)] Charlie is cold.[(triple4)] Charlie is not red.[(triple5)] Gary is cold.[(triple6)] Gary is young.[(triple7)] @1: Anne is red.[(((triple1) -> rule6))] Gary is green.[(((triple7) -> rule3))] @2: Anne is smart.[(((triple1 ((triple1) -> rule6)) -> rule4))] @3: Anne is young.[(((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2))] @4: Anne is green.[(((((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2)) -> rule3))] @5: Anne is cold.[(((((((((triple1 ((triple1) -> rule6)) -> rule4)) -> rule2)) -> rule3) triple1) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is not green.
("Bob" "is" "green" "-")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is not red.
("Charlie" "is" "red" "-")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple7) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
((((((triple1 ((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
((((((((triple1 ((triple1) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5