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