Anne is kind. Charlie is nice. Charlie is red. Charlie is young. Dave is red. Dave is white. Dave is young. Erin is nice. Erin is white. Erin is young. All young people are red. All kind people are young. If someone is kind and rough then they are red. If Anne is nice and Anne is white then Anne is young. Kind, rough people are white. All kind, red people are rough. Red, white people are nice.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and rough then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Anne is nice and Anne is white then Anne is young.
((("Anne" "is" "nice" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "young" "+"))
Kind, rough people are white.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
All kind, red people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Red, white people are nice.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Charlie is young.
True
1
proof
[(triple4)]
("Charlie" "is" "young" "+")
triple4
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Dave is nice.
True
3
proof
[(((triple5 triple6) -> rule7) OR ((((triple7) -> rule1) triple6) -> rule7))]
("Dave" "is" "nice" "+")
((triple5 triple6) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple7) -> (rule1 % int2)) triple6) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Erin is not red.
False
2
inv-proof
[(((triple10) -> rule1))]
("Erin" "is" "red" "-")
((triple10) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Anne is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is rough.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6))]
("Anne" "is" "rough" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not rough.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6))]
("Anne" "is" "rough" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is white.
True
7
proof
[(((triple1 ((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6)) -> rule5))]
("Anne" "is" "white" "+")
((triple1 ((triple1 ((((triple1) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is not white.
False
7
inv-proof
[(((triple1 ((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6)) -> rule5))]
("Anne" "is" "white" "-")
((triple1 ((triple1 ((((triple1) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is nice.
True
11
proof
[(((((((triple1) -> rule2)) -> rule1) ((triple1 ((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6)) -> rule5)) -> rule7))]
("Anne" "is" "nice" "+")
((((((triple1) -> (rule2 % int5))) -> (rule1 % int4)) ((triple1 ((triple1 ((((triple1) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Anne is not nice.
False
11
inv-proof
[(((((((triple1) -> rule2)) -> rule1) ((triple1 ((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6)) -> rule5)) -> rule7))]
("Anne" "is" "nice" "-")
((((((triple1) -> (rule2 % int5))) -> (rule1 % int4)) ((triple1 ((triple1 ((((triple1) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "rough" "+")
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "rough" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Charlie is nice.[(triple2)] Charlie is red.[(triple3 OR ((triple4) -> rule1))] Charlie is young.[(triple4)] Dave is red.[(triple5 OR ((triple7) -> rule1))] Dave is white.[(triple6)] Dave is young.[(triple7)] Erin is nice.[(triple8 OR ((((triple10) -> rule1) triple9) -> rule7))] Erin is white.[(triple9)] Erin is young.[(triple10)] @1: Anne is young.[(((triple1) -> rule2))] Dave is nice.[(((triple5 triple6) -> rule7) OR ((((triple7) -> rule1) triple6) -> rule7))] Erin is red.[(((triple10) -> rule1))] @2: Anne is red.[(((((triple1) -> rule2)) -> rule1))] @3: Anne is rough.[(((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6))] @4: Anne is white.[(((triple1 ((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6)) -> rule5))] @5: Anne is nice.[(((((((triple1) -> rule2)) -> rule1) ((triple1 ((triple1 ((((triple1) -> rule2)) -> rule1)) -> rule6)) -> rule5)) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
((triple4) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
((((triple10) -> (rule1 % int2)) triple9) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple5 triple6) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple7) -> (rule1 % int2)) triple6) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple10) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((triple1 ((triple1 ((((triple1) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple1) -> (rule2 % int5))) -> (rule1 % int4)) ((triple1 ((triple1 ((((triple1) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5