Charlie is green. Charlie is nice. Dave is blue. Dave is kind. Dave is quiet. Dave is round. Fiona is green. Fiona is kind. Fiona is round. Fiona is white. Blue things are white. If something is green then it is nice. If something is white and kind then it is green.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is white and kind then it is green.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Charlie is nice.
True
1
proof
[(triple2 OR ((triple1) -> rule2))]
("Charlie" "is" "nice" "+")
triple2
((triple1) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is not quiet.
False
1
inv-proof
[(triple5)]
("Dave" "is" "quiet" "-")
triple5
Dave is white.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "white" "+")
((triple3) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "white" "-")
((triple3) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
True
4
proof
[(((((triple3) -> rule1) triple4) -> rule3))]
("Dave" "is" "green" "+")
((((triple3) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not green.
False
4
inv-proof
[(((((triple3) -> rule1) triple4) -> rule3))]
("Dave" "is" "green" "-")
((((triple3) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
True
5
proof
[(((((((triple3) -> rule1) triple4) -> rule3)) -> rule2))]
("Dave" "is" "nice" "+")
((((((triple3) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is not nice.
False
5
inv-proof
[(((((((triple3) -> rule1) triple4) -> rule3)) -> rule2))]
("Dave" "is" "nice" "-")
((((((triple3) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not round.
Unknown
inv-random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Charlie is green.[(triple1)] Charlie is nice.[(triple2 OR ((triple1) -> rule2))] Dave is blue.[(triple3)] Dave is kind.[(triple4)] Dave is quiet.[(triple5)] Dave is round.[(triple6)] Fiona is green.[(triple7 OR ((triple10 triple8) -> rule3))] Fiona is kind.[(triple8)] Fiona is round.[(triple9)] Fiona is white.[(triple10)] @1: Dave is white.[(((triple3) -> rule1))] Fiona is nice.[(((triple7) -> rule2) OR ((((triple10 triple8) -> rule3)) -> rule2))] @2: Dave is green.[(((((triple3) -> rule1) triple4) -> rule3))] @3: Dave is nice.[(((((((triple3) -> rule1) triple4) -> rule3)) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
((triple1) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
((triple10 triple8) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Fiona is white.
("Fiona" "is" "white" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple7) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple10 triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple3) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple3) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3