Dave is blue. Dave is green. Dave is kind. Dave is quiet. Dave is round. Dave is smart. Erin is green. Erin is kind. Erin is quiet. Fiona is blue. Fiona is quiet. Gary is big. Gary is quiet. Gary is round. Gary is smart. Green things are smart. If Erin is blue then Erin is round. All kind things are quiet. If Gary is round then Gary is kind. All kind things are smart. All green things are round.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Erin is blue then Erin is round.
((("Erin" "is" "blue" "+")) -> ("Erin" "is" "round" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If Gary is round then Gary is kind.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "kind" "+"))
All kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Erin is quiet.
True
1
proof
[(triple9 OR ((triple8) -> rule3))]
("Erin" "is" "quiet" "+")
triple9
((triple8) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Dave is not smart.
False
1
inv-proof
[(triple6 OR ((triple2) -> rule1) OR ((triple3) -> rule5))]
("Dave" "is" "smart" "-")
triple6
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple3) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
True
2
proof
[(((triple7) -> rule1) OR ((triple8) -> rule5))]
("Erin" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple8) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple7) -> rule6))]
("Erin" "is" "round" "-")
((triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Dave is blue.[(triple1)] Dave is green.[(triple2)] Dave is kind.[(triple3)] Dave is quiet.[(triple4 OR ((triple3) -> rule3))] Dave is round.[(triple5 OR ((triple2) -> rule6))] Dave is smart.[(triple6 OR ((triple2) -> rule1) OR ((triple3) -> rule5))] Erin is green.[(triple7)] Erin is kind.[(triple8)] Erin is quiet.[(triple9 OR ((triple8) -> rule3))] Fiona is blue.[(triple10)] Fiona is quiet.[(triple11)] Gary is big.[(triple12)] Gary is quiet.[(triple13 OR ((((triple14) -> rule4)) -> rule3))] Gary is round.[(triple14)] Gary is smart.[(triple15 OR ((((triple14) -> rule4)) -> rule5))] @1: Erin is round.[(((triple7) -> rule6))] Erin is smart.[(((triple7) -> rule1) OR ((triple8) -> rule5))] Gary is kind.[(((triple14) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
((triple3) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple2) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple6
((triple2) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple3) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple7
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple8) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Gary is big.
("Gary" "is" "big" "+")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
((((triple14) -> (rule4 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
((((triple14) -> (rule4 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple7) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple8) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple14) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1