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