Charlie is round. Dave is not green. Erin is young. Gary is blue. If someone is young then they are white. If someone is green and blue then they are white. Round people are young. White people are not rough. If Erin is not round then Erin is rough. If someone is young then they are not quiet.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is not green.
("Dave" "is" "green" "-")
Erin is young.
("Erin" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is green and blue then they are white.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
White people are not rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "-"))
If Erin is not round then Erin is rough.
((("Erin" "is" "round" "~")) -> ("Erin" "is" "rough" "+"))
If someone is young then they are not quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "-"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Erin is not young.
False
1
inv-proof
[(triple3)]
("Erin" "is" "young" "-")
triple3
Charlie is young.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "young" "+")
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "young" "-")
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not rough.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule4))]
("Charlie" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule4))]
("Charlie" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Gary is white.
Unknown
rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "young" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is round.[(triple1)] Dave is not green.[(triple2)] Erin is young.[(triple3)] Gary is blue.[(triple4)] @1: Charlie is young.[(((triple1) -> rule3))] Erin is not quiet.[(((triple3) -> rule6))] Erin is white.[(((triple3) -> rule1))] @2: Charlie is not quiet.[(((((triple1) -> rule3)) -> rule6))] Charlie is white.[(((((triple1) -> rule3)) -> rule1))] Erin is not rough.[(((((triple3) -> rule1)) -> rule4))] @3: Charlie is not rough.[(((((((triple1) -> rule3)) -> rule1)) -> rule4))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is not green.
("Dave" "is" "green" "-")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is not quiet.
("Erin" "is" "quiet" "-")
((triple3) -> (rule6 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple3) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Charlie is not rough.
("Charlie" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3