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