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