Dave is big. Erin is quiet. Gary is young. If someone is white then they are young. If someone is white then they are quiet. If Dave is young then Dave is cold. If someone is big then they are young. Young, cold people are quiet. White, big people are young.
Dave is big.
("Dave" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is white then they are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Dave is young then Dave is cold.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "cold" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Young, cold people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
White, big people are young.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is young.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "young" "+")
((triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "young" "-")
((triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Dave" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Dave" "is" "cold" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is quiet.
True
6
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule5))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not quiet.
False
6
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule5))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "young" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Dave is big.[(triple1)] Erin is quiet.[(triple2)] Gary is young.[(triple3)] @1: Dave is young.[(((triple1) -> rule4))] @2: Dave is cold.[(((((triple1) -> rule4)) -> rule3))] @3: Dave is quiet.[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3