Charlie is blue. Charlie is green. Charlie is nice. Charlie is quiet. Charlie is round. Charlie is smart. Charlie is white. Fiona is blue. Fiona is green. Fiona is nice. Fiona is quiet. Fiona is white. Gary is nice. Gary is quiet. Gary is round. Quiet people are nice. If someone is green and smart then they are white. If someone is blue then they are smart.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is green and smart then they are white.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Charlie is green.
True
1
proof
[(triple2)]
("Charlie" "is" "green" "+")
triple2
Charlie is not white.
False
1
inv-proof
[(triple7 OR ((triple2 triple6) -> rule2) OR ((triple2 ((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "white" "-")
triple7
((triple2 triple6) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple2 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Fiona is smart.
True
2
proof
[(((triple8) -> rule3))]
("Fiona" "is" "smart" "+")
((triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple8) -> rule3))]
("Fiona" "is" "smart" "-")
((triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2)] Charlie is nice.[(triple3 OR ((triple4) -> rule1))] Charlie is quiet.[(triple4)] Charlie is round.[(triple5)] Charlie is smart.[(triple6 OR ((triple1) -> rule3))] Charlie is white.[(triple7 OR ((triple2 triple6) -> rule2) OR ((triple2 ((triple1) -> rule3)) -> rule2))] Fiona is blue.[(triple8)] Fiona is green.[(triple9)] Fiona is nice.[(triple10 OR ((triple11) -> rule1))] Fiona is quiet.[(triple11)] Fiona is white.[(triple12 OR ((triple9 ((triple8) -> rule3)) -> rule2))] Gary is nice.[(triple13 OR ((triple14) -> rule1))] Gary is quiet.[(triple14)] Gary is round.[(triple15)] @1: Fiona is smart.[(((triple8) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple4) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple1) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple2 triple6) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple2 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
((triple11) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is white.
("Fiona" "is" "white" "+")
triple12
((triple9 ((triple8) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple13
((triple14) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is round.
("Gary" "is" "round" "+")
triple15
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1