Bob is young. Dave is big. Harry is big. All young things are big. If Harry is big then Harry is quiet. If Bob is green then Bob is young. If Bob is big and Bob is not young then Bob is blue. If something is quiet then it is round. All blue things are quiet. Big things are quiet. All big things are quiet.
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If Harry is big then Harry is quiet.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "quiet" "+"))
If Bob is green then Bob is young.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "young" "+"))
If Bob is big and Bob is not young then Bob is blue.
((("Bob" "is" "big" "+") ("Bob" "is" "young" "~")) -> ("Bob" "is" "blue" "+"))
If something is quiet then it is round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All big things are quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Bob is young.
True
1
proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Bob is not young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple3) -> rule2) OR ((triple3) -> rule7) OR ((triple3) -> rule8))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple3) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple3) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple3) -> rule2) OR ((triple3) -> rule7) OR ((triple3) -> rule8))]
("Harry" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple3) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple3) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule1)) -> rule8))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule1)) -> rule8))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is round.
True
4
proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule5) OR ((((((triple1) -> rule1)) -> rule8)) -> rule5))]
("Bob" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not round.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule7)) -> rule5) OR ((((((triple1) -> rule1)) -> rule8)) -> rule5))]
("Bob" "is" "round" "-")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is young.[(triple1)] Dave is big.[(triple2)] Harry is big.[(triple3)] @1: Bob is big.[(((triple1) -> rule1))] Dave is quiet.[(((triple2) -> rule7) OR ((triple2) -> rule8))] Harry is quiet.[(((triple3) -> rule2) OR ((triple3) -> rule7) OR ((triple3) -> rule8))] @2: Bob is quiet.[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule1)) -> rule8))] Dave is round.[(((((triple2) -> rule7)) -> rule5) OR ((((triple2) -> rule8)) -> rule5))] Harry is round.[(((((triple3) -> rule2)) -> rule5) OR ((((triple3) -> rule7)) -> rule5) OR ((((triple3) -> rule8)) -> rule5))] @3: Bob is round.[(((((((triple1) -> rule1)) -> rule7)) -> rule5) OR ((((((triple1) -> rule1)) -> rule8)) -> rule5))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple2) -> (rule8 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple3) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple3) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3