Charlie is rough. Harry is blue. If Harry is cold then Harry is rough. If Harry is cold then Harry is not green. Nice people are green. If Charlie is rough then Charlie is nice. All cold, green people are smart. Green people are smart.
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If Harry is cold then Harry is rough.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "rough" "+"))
If Harry is cold then Harry is not green.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "green" "-"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Charlie is rough then Charlie is nice.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "nice" "+"))
All cold, green people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple2)]
("Harry" "is" "blue" "-")
triple2
Charlie is nice.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("Charlie" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not green.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("Charlie" "is" "green" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
True
4
proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule6))]
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not smart.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule3)) -> rule6))]
("Charlie" "is" "smart" "-")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Harry" "is" "smart" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is rough.[(triple1)] Harry is blue.[(triple2)] @1: Charlie is nice.[(((triple1) -> rule4))] @2: Charlie is green.[(((((triple1) -> rule4)) -> rule3))] @3: Charlie is smart.[(((((((triple1) -> rule4)) -> rule3)) -> rule6))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3