Anne is nice. Anne is rough. Anne is white. Charlie is big. Charlie is green. Charlie is not rough. Erin is green. Erin is rough. Erin is young. Gary is big. Gary is green. Gary is nice. Gary is rough. Gary is smart. Gary is white. Gary is not young. All big things are nice. If Charlie is nice then Charlie is white. If Erin is green then Erin is smart. All green, white things are smart. White things are smart. If something is young and not white then it is smart.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is not young.
("Gary" "is" "young" "-")
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Charlie is nice then Charlie is white.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "white" "+"))
If Erin is green then Erin is smart.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "smart" "+"))
All green, white things are smart.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
White things are smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If something is young and not white then it is smart.
((("something" "is" "young" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "+"))
Gary is big.
True
1
proof
[(triple10)]
("Gary" "is" "big" "+")
triple10
Gary is not big.
False
1
inv-proof
[(triple10)]
("Gary" "is" "big" "-")
triple10
Charlie is nice.
True
2
proof
[(((triple4) -> rule1))]
("Charlie" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple7) -> rule3))]
("Erin" "is" "smart" "-")
((triple7) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is white.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Charlie" "is" "white" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not white.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Charlie" "is" "white" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
True
4
proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule5) OR ((triple5 ((((triple4) -> rule1)) -> rule2)) -> rule4))]
("Charlie" "is" "smart" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((triple5 ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not smart.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule5) OR ((triple5 ((((triple4) -> rule1)) -> rule2)) -> rule4))]
("Charlie" "is" "smart" "-")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((triple5 ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is nice.[(triple1)] Anne is rough.[(triple2)] Anne is white.[(triple3)] Charlie is big.[(triple4)] Charlie is green.[(triple5)] Charlie is not rough.[(triple6)] Erin is green.[(triple7)] Erin is rough.[(triple8)] Erin is young.[(triple9)] Gary is big.[(triple10)] Gary is green.[(triple11)] Gary is nice.[(triple12 OR ((triple10) -> rule1))] Gary is not young.[(triple16)] Gary is rough.[(triple13)] Gary is smart.[(triple14 OR ((triple15) -> rule5) OR ((triple11 triple15) -> rule4))] Gary is white.[(triple15)] @1: Anne is smart.[(((triple3) -> rule5))] Charlie is nice.[(((triple4) -> rule1))] Erin is smart.[(((triple7) -> rule3))] @2: Charlie is white.[(((((triple4) -> rule1)) -> rule2))] @3: Charlie is smart.[(((((((triple4) -> rule1)) -> rule2)) -> rule5) OR ((triple5 ((((triple4) -> rule1)) -> rule2)) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
Gary is green.
("Gary" "is" "green" "+")
triple11
Gary is nice.
("Gary" "is" "nice" "+")
triple12
((triple10) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not young.
("Gary" "is" "young" "-")
triple16
Gary is rough.
("Gary" "is" "rough" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
((triple15) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple11 triple15) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple15
Anne is smart.
("Anne" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((triple5 ((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3