Dave is kind. Dave is quiet. Dave is rough. Dave is round. Dave is smart. Erin is big. Erin is nice. Erin is quiet. Gary is nice. Gary is quiet. Gary is round. Gary is smart. All smart people are big. If someone is smart and big then they are nice. All kind, smart people are nice. All kind, quiet people are nice. Rough, big people are round. Round people are nice. Smart people are round. All rough, big people are nice.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is smart and big then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All kind, smart people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All kind, quiet people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Rough, big people are round.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All rough, big people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Dave is round.
True
1
proof
[(triple4 OR ((triple5) -> rule7) OR ((triple3 ((triple5) -> rule1)) -> rule5))]
("Dave" "is" "round" "+")
triple4
((triple5) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple3 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Erin is not nice.
False
1
inv-proof
[(triple7)]
("Erin" "is" "nice" "-")
triple7
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Dave is kind.[(triple1)] Dave is quiet.[(triple2)] Dave is rough.[(triple3)] Dave is round.[(triple4 OR ((triple5) -> rule7) OR ((triple3 ((triple5) -> rule1)) -> rule5))] Dave is smart.[(triple5)] Erin is big.[(triple6)] Erin is nice.[(triple7)] Erin is quiet.[(triple8)] Gary is nice.[(triple9 OR ((triple11) -> rule6) OR ((((triple12) -> rule7)) -> rule6) OR ((triple12 ((triple12) -> rule1)) -> rule2))] Gary is quiet.[(triple10)] Gary is round.[(triple11 OR ((triple12) -> rule7))] Gary is smart.[(triple12)] @1: Dave is big.[(((triple5) -> rule1))] Dave is nice.[(((triple4) -> rule6) OR ((triple1 triple2) -> rule4) OR ((triple1 triple5) -> rule3) OR ((((triple5) -> rule7)) -> rule6) OR ((triple3 ((triple5) -> rule1)) -> rule8) OR ((triple5 ((triple5) -> rule1)) -> rule2) OR ((((triple3 ((triple5) -> rule1)) -> rule5)) -> rule6))] Gary is big.[(((triple12) -> rule1))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple5) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple3 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
((triple11) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple12) -> (rule7 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((triple12 ((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
((triple12) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Dave is big.
("Dave" "is" "big" "+")
((triple5) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple4) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple1 triple2) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple1 triple5) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((triple3 ((triple5) -> (rule1 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple5 ((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple3 ((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((triple12) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1