Anne is nice. Anne is young. Charlie is green. Charlie is nice. Erin is big. Erin is nice. Erin is white. Erin is young. Harry is kind. Harry is white. If something is white then it is young. If something is green and nice then it is not young. If something is white and not green then it is not young. If something is young then it is white. If something is green and young then it is not nice. If something is white and not green then it is big. Smart, nice things are kind. If something is kind and not big then it is smart.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is green and nice then it is not young.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "-"))
If something is white and not green then it is not young.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "young" "-"))
If something is young then it is white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is green and young then it is not nice.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "-"))
If something is white and not green then it is big.
((("something" "is" "white" "+") ("something" "is" "green" "~")) -> ("something" "is" "big" "+"))
Smart, nice things are kind.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is kind and not big then it is smart.
((("something" "is" "kind" "+") ("something" "is" "big" "~")) -> ("something" "is" "smart" "+"))
Harry is white.
True
1
proof
[(triple10)]
("Harry" "is" "white" "+")
triple10
Erin is not white.
False
1
inv-proof
[(triple7 OR ((triple8) -> rule4))]
("Erin" "is" "white" "-")
triple7
((triple8) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is not young.
True
3
proof
[(((triple3 triple4) -> rule2))]
("Charlie" "is" "young" "-")
((triple3 triple4) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is young.
False
3
inv-proof
[(((triple3 triple4) -> rule2))]
("Charlie" "is" "young" "+")
((triple3 triple4) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "white" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Anne" "is" "kind" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is nice.[(triple1)] Anne is young.[(triple2)] Charlie is green.[(triple3)] Charlie is nice.[(triple4)] Erin is big.[(triple5)] Erin is nice.[(triple6)] Erin is white.[(triple7 OR ((triple8) -> rule4))] Erin is young.[(triple8 OR ((triple7) -> rule1))] Harry is kind.[(triple9)] Harry is white.[(triple10)] @1: Anne is white.[(((triple2) -> rule4))] Charlie is not young.[(((triple3 triple4) -> rule2))] Harry is young.[(((triple10) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple8) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple8
((triple7) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Anne is white.
("Anne" "is" "white" "+")
((triple2) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
((triple3 triple4) -> (rule2 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple10) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1