Erin is kind. Erin is rough. Gary is kind. If someone is kind then they are not young. If someone is kind then they are round. All round, rough people are green. If Erin is quiet and Erin is rough then Erin is red. If someone is round and not young then they are rough. Round, quiet people are rough. All kind, green people are rough. Red, young people are quiet.
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is kind then they are not young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "-"))
If someone is kind then they are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All round, rough people are green.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If Erin is quiet and Erin is rough then Erin is red.
((("Erin" "is" "quiet" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "red" "+"))
If someone is round and not young then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "rough" "+"))
Round, quiet people are rough.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All kind, green people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Red, young people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Erin is rough.
True
1
proof
[(triple2 OR ((((triple1) -> rule2) ((triple1) -> rule1)) -> rule5))]
("Erin" "is" "rough" "+")
triple2
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not kind.
False
1
inv-proof
[(triple1)]
("Erin" "is" "kind" "-")
triple1
Gary is not young.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "young" "-")
((triple3) -> (rule1 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is young.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "young" "+")
((triple3) -> (rule1 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Erin is green.
True
4
proof
[(((((triple1) -> rule2) triple2) -> rule3) OR ((((triple1) -> rule2) ((((triple1) -> rule2) ((triple1) -> rule1)) -> rule5)) -> rule3))]
("Erin" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple1) -> (rule2 % int4)) ((((triple1) -> (rule2 % int4)) ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Gary is not rough.
False
5
inv-proof
[(((((triple3) -> rule2) ((triple3) -> rule1)) -> rule5))]
("Gary" "is" "rough" "-")
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not young.
("Gary" "is" "young" "-")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is green.
True
8
proof
[(((((triple3) -> rule2) ((((triple3) -> rule2) ((triple3) -> rule1)) -> rule5)) -> rule3))]
("Gary" "is" "green" "+")
((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule2 % int4)) ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not young.
("Gary" "is" "young" "-")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is not green.
False
8
inv-proof
[(((((triple3) -> rule2) ((((triple3) -> rule2) ((triple3) -> rule1)) -> rule5)) -> rule3))]
("Gary" "is" "green" "-")
((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule2 % int4)) ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not young.
("Gary" "is" "young" "-")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "quiet" "-")
Erin is red.
Unknown
rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Erin" "is" "red" "+")
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "quiet" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Erin is kind.[(triple1)] Erin is rough.[(triple2 OR ((((triple1) -> rule2) ((triple1) -> rule1)) -> rule5))] Gary is kind.[(triple3)] @1: Erin is not young.[(((triple1) -> rule1))] Erin is round.[(((triple1) -> rule2))] Gary is not young.[(((triple3) -> rule1))] Gary is round.[(((triple3) -> rule2))] @2: Erin is green.[(((((triple1) -> rule2) triple2) -> rule3) OR ((((triple1) -> rule2) ((((triple1) -> rule2) ((triple1) -> rule1)) -> rule5)) -> rule3))] Gary is rough.[(((((triple3) -> rule2) ((triple3) -> rule1)) -> rule5))] @3: Gary is green.[(((((triple3) -> rule2) ((((triple3) -> rule2) ((triple3) -> rule1)) -> rule5)) -> rule3))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Erin is not young.
("Erin" "is" "young" "-")
((triple1) -> (rule1 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple1) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Gary is not young.
("Gary" "is" "young" "-")
((triple3) -> (rule1 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple1) -> (rule2 % int4)) ((((triple1) -> (rule2 % int4)) ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
((((triple3) -> (rule2 % int3)) ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not young.
("Gary" "is" "young" "-")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule2 % int4)) ((((triple3) -> (rule2 % int4)) ((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not young.
("Gary" "is" "young" "-")
int3
Gary is round.
("Gary" "is" "round" "+")
int4