Anne is red. Harry is cold. Cold things are red. All red things are rough. Cold things are rough. All rough, cold things are round. If something is round then it is not big. If something is green and not big then it is not blue.
Anne is red.
("Anne" "is" "red" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All red things are rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All rough, cold things are round.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is round then it is not big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "-"))
If something is green and not big then it is not blue.
((("something" "is" "green" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "-"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Harry is rough.
True
2
proof
[(((triple2) -> rule3) OR ((((triple2) -> rule1)) -> rule2))]
("Harry" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not rough.
False
2
inv-proof
[(((triple2) -> rule3) OR ((((triple2) -> rule1)) -> rule2))]
("Harry" "is" "rough" "-")
((triple2) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
True
4
proof
[(((((triple2) -> rule3) triple2) -> rule4) OR ((((((triple2) -> rule1)) -> rule2) triple2) -> rule4))]
("Harry" "is" "round" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not round.
False
4
inv-proof
[(((((triple2) -> rule3) triple2) -> rule4) OR ((((((triple2) -> rule1)) -> rule2) triple2) -> rule4))]
("Harry" "is" "round" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not big.
True
5
proof
[(((((((triple2) -> rule3) triple2) -> rule4)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule2) triple2) -> rule4)) -> rule5))]
("Harry" "is" "big" "-")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is big.
False
5
inv-proof
[(((((((triple2) -> rule3) triple2) -> rule4)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule2) triple2) -> rule4)) -> rule5))]
("Harry" "is" "big" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is red.[(triple1)] Harry is cold.[(triple2)] @1: Anne is rough.[(((triple1) -> rule2))] Harry is red.[(((triple2) -> rule1))] Harry is rough.[(((triple2) -> rule3) OR ((((triple2) -> rule1)) -> rule2))] @2: Harry is round.[(((((triple2) -> rule3) triple2) -> rule4) OR ((((((triple2) -> rule1)) -> rule2) triple2) -> rule4))] @3: Harry is not big.[(((((((triple2) -> rule3) triple2) -> rule4)) -> rule5) OR ((((((((triple2) -> rule1)) -> rule2) triple2) -> rule4)) -> rule5))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple2) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not big.
("Harry" "is" "big" "-")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4