Charlie is green. Dave is smart. Harry is smart. If Charlie is smart then Charlie is green. Cold, white people are nice. Big, rough people are cold. Green people are rough. Green people are big. If someone is cold and green then they are nice.
Charlie is green.
("Charlie" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Charlie is smart then Charlie is green.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "green" "+"))
Cold, white people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Big, rough people are cold.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and green then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "-")
triple3
Charlie is rough.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "big" "-")
((triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
True
5
proof
[(((((triple1) -> rule5) ((triple1) -> rule4)) -> rule3))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not cold.
False
5
inv-proof
[(((((triple1) -> rule5) ((triple1) -> rule4)) -> rule3))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is nice.
True
7
proof
[(((((((triple1) -> rule5) ((triple1) -> rule4)) -> rule3) triple1) -> rule6))]
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule5 % int4)) ((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is not nice.
False
7
inv-proof
[(((((((triple1) -> rule5) ((triple1) -> rule4)) -> rule3) triple1) -> rule6))]
("Charlie" "is" "nice" "-")
((((((triple1) -> (rule5 % int4)) ((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "rough" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is green.[(triple1)] Dave is smart.[(triple2)] Harry is smart.[(triple3)] @1: Charlie is big.[(((triple1) -> rule5))] Charlie is rough.[(((triple1) -> rule4))] @2: Charlie is cold.[(((((triple1) -> rule5) ((triple1) -> rule4)) -> rule3))] @3: Charlie is nice.[(((((((triple1) -> rule5) ((triple1) -> rule4)) -> rule3) triple1) -> rule6))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule5 % int3)) ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule5 % int4)) ((triple1) -> (rule4 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4