Anne is cold. Anne is quiet. Dave is cold. Dave is not quiet. Fiona is nice. Gary is not blue. Gary is round. If someone is blue then they are not rough. If Anne is cold then Anne is blue. If someone is cold and not blue then they are not nice. Nice, cold people are round. If Anne is not rough then Anne is nice. If someone is round and not nice then they are big. Cold, round people are big. All rough, cold people are big.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is round.
("Gary" "is" "round" "+")
If someone is blue then they are not rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "-"))
If Anne is cold then Anne is blue.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "blue" "+"))
If someone is cold and not blue then they are not nice.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "-"))
Nice, cold people are round.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If Anne is not rough then Anne is nice.
((("Anne" "is" "rough" "~")) -> ("Anne" "is" "nice" "+"))
If someone is round and not nice then they are big.
((("someone" "is" "round" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "big" "+"))
Cold, round people are big.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All rough, cold people are big.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Gary is round.
True
1
proof
[(triple7)]
("Gary" "is" "round" "+")
triple7
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is blue.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not rough.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule5))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not nice.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule5))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
True
6
proof
[(((((((((triple1) -> rule2)) -> rule1)) -> rule5) triple1) -> rule4))]
("Anne" "is" "round" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not rough.
("Anne" "is" "rough" "-")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is not round.
False
6
inv-proof
[(((((((((triple1) -> rule2)) -> rule1)) -> rule5) triple1) -> rule4))]
("Anne" "is" "round" "-")
((((((((triple1) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not rough.
("Anne" "is" "rough" "-")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is big.
True
8
proof
[(((triple1 ((((((((triple1) -> rule2)) -> rule1)) -> rule5) triple1) -> rule4)) -> rule7))]
("Anne" "is" "big" "+")
((triple1 ((((((((triple1) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not rough.
("Anne" "is" "rough" "-")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Anne is not big.
False
8
inv-proof
[(((triple1 ((((((((triple1) -> rule2)) -> rule1)) -> rule5) triple1) -> rule4)) -> rule7))]
("Anne" "is" "big" "-")
((triple1 ((((((((triple1) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not rough.
("Anne" "is" "rough" "-")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "big" "+")
Dave is not big.
Unknown
inv-rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Dave" "is" "big" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "big" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "round" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is quiet.[(triple2)] Dave is cold.[(triple3)] Dave is not quiet.[(triple4)] Fiona is nice.[(triple5)] Gary is not blue.[(triple6)] Gary is round.[(triple7)] @1: Anne is blue.[(((triple1) -> rule2))] @2: Anne is not rough.[(((((triple1) -> rule2)) -> rule1))] @3: Anne is nice.[(((((((triple1) -> rule2)) -> rule1)) -> rule5))] @4: Anne is round.[(((((((((triple1) -> rule2)) -> rule1)) -> rule5) triple1) -> rule4))] @5: Anne is big.[(((triple1 ((((((((triple1) -> rule2)) -> rule1)) -> rule5) triple1) -> rule4)) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Gary is not blue.
("Gary" "is" "blue" "-")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not rough.
("Anne" "is" "rough" "-")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
((triple1 ((((((((triple1) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not rough.
("Anne" "is" "rough" "-")
int4
Anne is blue.
("Anne" "is" "blue" "+")
int5