Bob is not big. Bob is green. Bob is rough. Bob is round. Bob is smart. Bob is not white. Dave is green. Dave is rough. Erin is not big. Erin is not rough. Erin is smart. Erin is young. If Bob is young and Bob is smart then Bob is rough. Young people are not white. All smart people are not white. If Bob is smart and Bob is not green then Bob is round. Rough people are smart. If someone is white and not smart then they are not round.
Bob is not big.
("Bob" "is" "big" "-")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is not white.
("Bob" "is" "white" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If Bob is young and Bob is smart then Bob is rough.
((("Bob" "is" "young" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "rough" "+"))
Young people are not white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "-"))
All smart people are not white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "-"))
If Bob is smart and Bob is not green then Bob is round.
((("Bob" "is" "smart" "+") ("Bob" "is" "green" "~")) -> ("Bob" "is" "round" "+"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is white and not smart then they are not round.
((("someone" "is" "white" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "round" "-"))
Erin is young.
True
1
proof
[(triple12)]
("Erin" "is" "young" "+")
triple12
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Erin is not white.
True
2
proof
[(((triple11) -> rule3) OR ((triple12) -> rule2))]
("Erin" "is" "white" "-")
((triple11) -> (rule3 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
((triple12) -> (rule2 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is white.
False
2
inv-proof
[(((triple11) -> rule3) OR ((triple12) -> rule2))]
("Erin" "is" "white" "+")
((triple11) -> (rule3 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
((triple12) -> (rule2 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Dave is not white.
True
3
proof
[(((((triple8) -> rule5)) -> rule3))]
("Dave" "is" "white" "-")
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is white.
False
3
inv-proof
[(((((triple8) -> rule5)) -> rule3))]
("Dave" "is" "white" "+")
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is green.[(triple2)] Bob is not big.[(triple1)] Bob is not white.[(triple6 OR ((triple5) -> rule3) OR ((((triple3) -> rule5)) -> rule3))] Bob is rough.[(triple3)] Bob is round.[(triple4)] Bob is smart.[(triple5 OR ((triple3) -> rule5))] Dave is green.[(triple7)] Dave is rough.[(triple8)] Erin is not big.[(triple9)] Erin is not rough.[(triple10)] Erin is smart.[(triple11)] Erin is young.[(triple12)] @1: Dave is smart.[(((triple8) -> rule5))] Erin is not white.[(((triple11) -> rule3) OR ((triple12) -> rule2))] @2: Dave is not white.[(((((triple8) -> rule5)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is not big.
("Bob" "is" "big" "-")
triple1
Bob is not white.
("Bob" "is" "white" "-")
triple6
((triple5) -> (rule3 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
((triple3) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Erin is not big.
("Erin" "is" "big" "-")
triple9
Erin is not rough.
("Erin" "is" "rough" "-")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
Dave is smart.
("Dave" "is" "smart" "+")
((triple8) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is not white.
("Erin" "is" "white" "-")
((triple11) -> (rule3 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
((triple12) -> (rule2 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Dave is not white.
("Dave" "is" "white" "-")
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2