Bob is blue. If Bob is smart then Bob is round. Round things are smart. Quiet, young things are round. If something is blue and quiet then it is smart. If something is young and blue then it is nice. If something is blue and nice then it is big. Blue things are young. All smart things are big.
Bob is blue.
("Bob" "is" "blue" "+")
If Bob is smart then Bob is round.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "round" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Quiet, young things are round.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is blue and quiet then it is smart.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
If something is young and blue then it is nice.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is blue and nice then it is big.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is young.
True
2
proof
[(((triple1) -> rule7))]
("Bob" "is" "young" "+")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule7))]
("Bob" "is" "young" "-")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
True
4
proof
[(((((triple1) -> rule7) triple1) -> rule5))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not nice.
False
4
inv-proof
[(((((triple1) -> rule7) triple1) -> rule5))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@3: Bob is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule4 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is round.
Unknown
rconc
[@3: Bob is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is blue.[(triple1)] @1: Bob is young.[(((triple1) -> rule7))] @2: Bob is nice.[(((((triple1) -> rule7) triple1) -> rule5))] @3: Bob is big.[(((triple1 ((((triple1) -> rule7) triple1) -> rule5)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((triple1 ((((triple1) -> (rule7 % int3)) triple1) -> (rule5 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3