Bob is nice. Dave is smart. Erin is quiet. Harry is quiet. All quiet things are big. Big things are not young. All nice things are round.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Big things are not young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "-"))
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Erin is not quiet.
False
1
inv-proof
[(triple3)]
("Erin" "is" "quiet" "-")
triple3
Bob is round.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "round" "+")
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "big" "-")
((triple3) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Dave is big.
Unknown
rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "big" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is nice.[(triple1)] Dave is smart.[(triple2)] Erin is quiet.[(triple3)] Harry is quiet.[(triple4)] @1: Bob is round.[(((triple1) -> rule3))] Erin is big.[(((triple3) -> rule1))] Harry is big.[(((triple4) -> rule1))] @2: Erin is not young.[(((((triple3) -> rule1)) -> rule2))] Harry is not young.[(((((triple4) -> rule1)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Erin is not young.
("Erin" "is" "young" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Harry is not young.
("Harry" "is" "young" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
int2