Charlie is big. Charlie is nice. Charlie is rough. Dave is big. Dave is quiet. Erin is white. Fiona is rough. If Dave is green then Dave is nice. If someone is green then they are quiet. All big people are green. Nice, big people are white. All nice, big people are rough. Red, big people are white.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If Dave is green then Dave is nice.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "nice" "+"))
If someone is green then they are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Nice, big people are white.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
All nice, big people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Red, big people are white.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Dave is big.
True
1
proof
[(triple4)]
("Dave" "is" "big" "+")
triple4
Dave is not quiet.
False
1
inv-proof
[(triple5 OR ((((triple4) -> rule3)) -> rule2))]
("Dave" "is" "quiet" "-")
triple5
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Charlie is green.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "green" "-")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is nice.
True
3
proof
[(((((triple4) -> rule3)) -> rule1))]
("Dave" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Dave is white.
True
5
proof
[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule4))]
("Dave" "is" "white" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not rough.
False
5
inv-proof
[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule5))]
("Dave" "is" "rough" "-")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "rough" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Erin is quiet.
Unknown
rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "quiet" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Charlie is big.[(triple1)] Charlie is nice.[(triple2)] Charlie is rough.[(triple3 OR ((triple2 triple1) -> rule5))] Dave is big.[(triple4)] Dave is quiet.[(triple5 OR ((((triple4) -> rule3)) -> rule2))] Erin is white.[(triple6)] Fiona is rough.[(triple7)] @1: Charlie is green.[(((triple1) -> rule3))] Charlie is white.[(((triple2 triple1) -> rule4))] Dave is green.[(((triple4) -> rule3))] @2: Charlie is quiet.[(((((triple1) -> rule3)) -> rule2))] Dave is nice.[(((((triple4) -> rule3)) -> rule1))] @3: Dave is rough.[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule5))] Dave is white.[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
((triple2 triple1) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2 triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3