Charlie is big. Dave is quiet. Fiona is big. Red, rough people are big. All white, rough people are quiet. All nice people are quiet. Quiet people are nice. Rough people are white. All nice people are white. If Dave is quiet and Dave is red then Dave is big. Quiet people are rough.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Red, rough people are big.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All white, rough people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If Dave is quiet and Dave is red then Dave is big.
((("Dave" "is" "quiet" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "big" "+"))
Quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Dave is rough.
True
2
proof
[(((triple2) -> rule8))]
("Dave" "is" "rough" "+")
((triple2) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "nice" "-")
((triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
True
3
proof
[(((((triple2) -> rule4)) -> rule6) OR ((((triple2) -> rule8)) -> rule5))]
("Dave" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule6) OR ((((triple2) -> rule8)) -> rule5))]
("Dave" "is" "white" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Charlie is not quiet.
Unknown
inv-rconc
[@4: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@4: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule3 <- rule4 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Charlie is big.[(triple1)] Dave is quiet.[(triple2)] Fiona is big.[(triple3)] @1: Dave is nice.[(((triple2) -> rule4))] Dave is rough.[(((triple2) -> rule8))] @2: Dave is white.[(((((triple2) -> rule4)) -> rule6) OR ((((triple2) -> rule8)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule8 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2