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