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