Anne is round. Charlie is cold. Gary is kind. Harry is round. Cold things are kind. Rough things are big. All kind things are not rough. If something is kind and not rough then it is not red. All big, red things are blue. Cold things are not blue.
Anne is round.
("Anne" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All kind things are not rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "-"))
If something is kind and not rough then it is not red.
((("something" "is" "kind" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "-"))
All big, red things are blue.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Cold things are not blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "-"))
Harry is round.
True
1
proof
[(triple4)]
("Harry" "is" "round" "+")
triple4
Gary is not kind.
False
1
inv-proof
[(triple3)]
("Gary" "is" "kind" "-")
triple3
Charlie is not blue.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "blue" "-")
((triple2) -> (rule6 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is not red.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Gary" "is" "red" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Gary is red.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Gary" "is" "red" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Charlie is not red.
True
6
proof
[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule4))]
("Charlie" "is" "red" "-")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is red.
False
6
inv-proof
[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule4))]
("Charlie" "is" "red" "+")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "big" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "big" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is round.[(triple1)] Charlie is cold.[(triple2)] Gary is kind.[(triple3)] Harry is round.[(triple4)] @1: Charlie is kind.[(((triple2) -> rule1))] Charlie is not blue.[(((triple2) -> rule6))] Gary is not rough.[(((triple3) -> rule3))] @2: Charlie is not rough.[(((((triple2) -> rule1)) -> rule3))] Gary is not red.[(((triple3 ((triple3) -> rule3)) -> rule4))] @3: Charlie is not red.[(((((triple2) -> rule1) ((((triple2) -> rule1)) -> rule3)) -> rule4))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
((triple2) -> (rule6 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Gary is not red.
("Gary" "is" "red" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
int2
Charlie is not red.
("Charlie" "is" "red" "-")
((((triple2) -> (rule1 % int3)) ((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3