Charlie is big. Charlie is rough. Dave is not rough. Dave is round. Erin is rough. Gary is not quiet. Gary is not rough. All rough things are quiet. Quiet things are white. If something is young and not white then it is cold.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is round.
("Dave" "is" "round" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is not rough.
("Gary" "is" "rough" "-")
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is young and not white then it is cold.
((("something" "is" "young" "+") ("something" "is" "white" "~")) -> ("something" "is" "cold" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Dave is not round.
False
1
inv-proof
[(triple4)]
("Dave" "is" "round" "-")
triple4
Charlie is quiet.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple5) -> rule1))]
("Erin" "is" "quiet" "-")
((triple5) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("Erin" "is" "white" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Charlie" "is" "white" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "+")
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is big.[(triple1)] Charlie is rough.[(triple2)] Dave is not rough.[(triple3)] Dave is round.[(triple4)] Erin is rough.[(triple5)] Gary is not quiet.[(triple6)] Gary is not rough.[(triple7)] @1: Charlie is quiet.[(((triple2) -> rule1))] Erin is quiet.[(((triple5) -> rule1))] @2: Charlie is white.[(((((triple2) -> rule1)) -> rule2))] Erin is white.[(((((triple5) -> rule1)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is not rough.
("Dave" "is" "rough" "-")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple6
Gary is not rough.
("Gary" "is" "rough" "-")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple5) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2