Anne is round. Anne is not young. Fiona is green. Fiona is not round. Gary is white. Harry is kind. Harry is round. If someone is big then they are green. All big, red people are green. All green, red people are big. If someone is kind then they are red. If someone is green then they are kind. If someone is big then they are not young. If someone is green and not big then they are young. If someone is kind and not young then they are white.
Anne is round.
("Anne" "is" "round" "+")
Anne is not young.
("Anne" "is" "young" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Gary is white.
("Gary" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is big then they are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All big, red people are green.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All green, red people are big.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is kind then they are red.
((("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is big then they are not young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "-"))
If someone is green and not big then they are young.
((("someone" "is" "green" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "young" "+"))
If someone is kind and not young then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "white" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Harry is not kind.
False
1
inv-proof
[(triple6)]
("Harry" "is" "kind" "-")
triple6
Fiona is kind.
True
2
proof
[(((triple3) -> rule5))]
("Fiona" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple3) -> rule5))]
("Fiona" "is" "kind" "-")
((triple3) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is red.
True
3
proof
[(((((triple3) -> rule5)) -> rule4))]
("Fiona" "is" "red" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule4))]
("Fiona" "is" "red" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
True
5
proof
[(((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3))]
("Fiona" "is" "big" "+")
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not big.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3))]
("Fiona" "is" "big" "-")
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not young.
True
6
proof
[(((((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3)) -> rule6))]
("Fiona" "is" "young" "-")
((((triple3 ((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is young.
False
6
inv-proof
[(((((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3)) -> rule6))]
("Fiona" "is" "young" "+")
((((triple3 ((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is white.
True
9
proof
[(((((triple3) -> rule5) ((((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3)) -> rule6)) -> rule8))]
("Fiona" "is" "white" "+")
((((triple3) -> (rule5 % int5)) ((((triple3 ((((triple3) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not young.
("Fiona" "is" "young" "-")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Fiona is not white.
False
9
inv-proof
[(((((triple3) -> rule5) ((((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3)) -> rule6)) -> rule8))]
("Fiona" "is" "white" "-")
((((triple3) -> (rule5 % int5)) ((((triple3 ((((triple3) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not young.
("Fiona" "is" "young" "-")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is green.
Unknown
rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Gary is kind.
Unknown
rconc
[@4: Gary is kind.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule3 <- rule2 <- FAIL)]]
("Gary" "is" "kind" "+")
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Gary" "is" "big" "-")
Anne is big.
Unknown
rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is not young.[(triple2)] Anne is round.[(triple1)] Fiona is green.[(triple3)] Fiona is not round.[(triple4)] Gary is white.[(triple5)] Harry is kind.[(triple6)] Harry is round.[(triple7)] @1: Fiona is kind.[(((triple3) -> rule5))] Harry is red.[(((triple6) -> rule4))] @2: Fiona is red.[(((((triple3) -> rule5)) -> rule4))] @3: Fiona is big.[(((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3))] @4: Fiona is not young.[(((((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3)) -> rule6))] @5: Fiona is white.[(((((triple3) -> rule5) ((((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule3)) -> rule6)) -> rule8))]
Anne is not young.
("Anne" "is" "young" "-")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Fiona is not round.
("Fiona" "is" "round" "-")
triple4
Gary is white.
("Gary" "is" "white" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple3) -> (rule5 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple6) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not young.
("Fiona" "is" "young" "-")
((((triple3 ((((triple3) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
((((triple3) -> (rule5 % int5)) ((((triple3 ((((triple3) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is not young.
("Fiona" "is" "young" "-")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
int5