Charlie is big. Charlie is rough. Charlie is round. Charlie is white. Dave is cold. Dave is white. Erin is cold. Green people are cold. White people are green. Green, round people are rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
White people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Green, round people are rough.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Charlie is round.
True
1
proof
[(triple3)]
("Charlie" "is" "round" "+")
triple3
Charlie is not round.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "round" "-")
triple3
Dave is green.
True
2
proof
[(((triple6) -> rule2))]
("Dave" "is" "green" "+")
((triple6) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple4) -> rule2))]
("Charlie" "is" "green" "-")
((triple4) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "green" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "rough" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is big.[(triple1)] Charlie is rough.[(triple2 OR ((((triple4) -> rule2) triple3) -> rule3))] Charlie is round.[(triple3)] Charlie is white.[(triple4)] Dave is cold.[(triple5 OR ((((triple6) -> rule2)) -> rule1))] Dave is white.[(triple6)] Erin is cold.[(triple7)] @1: Charlie is green.[(((triple4) -> rule2))] Dave is green.[(((triple6) -> rule2))] @2: Charlie is cold.[(((((triple4) -> rule2)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
((((triple4) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple4) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple6) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2