Bob is big. Bob is round. Bob is young. Dave is big. Dave is furry. Dave is round. Erin is big. Erin is furry. Erin is quiet. Erin is rough. Erin is round. Erin is young. Harry is green. Harry is quiet. Harry is young. All rough things are big. If something is young then it is round. Green, quiet things are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is young then it is round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Green, quiet things are young.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Erin is round.
True
1
proof
[(triple11 OR ((triple12) -> rule2))]
("Erin" "is" "round" "+")
triple11
((triple12) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not quiet.
False
1
inv-proof
[(triple9)]
("Erin" "is" "quiet" "-")
triple9
Harry is round.
True
2
proof
[(((triple15) -> rule2) OR ((((triple13 triple14) -> rule3)) -> rule2))]
("Harry" "is" "round" "+")
((triple15) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple13 triple14) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not round.
False
2
inv-proof
[(((triple15) -> rule2) OR ((((triple13 triple14) -> rule3)) -> rule2))]
("Harry" "is" "round" "-")
((triple15) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple13 triple14) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "young" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is big.[(triple1)] Bob is round.[(triple2 OR ((triple3) -> rule2))] Bob is young.[(triple3)] Dave is big.[(triple4)] Dave is furry.[(triple5)] Dave is round.[(triple6)] Erin is big.[(triple7 OR ((triple10) -> rule1))] Erin is furry.[(triple8)] Erin is quiet.[(triple9)] Erin is rough.[(triple10)] Erin is round.[(triple11 OR ((triple12) -> rule2))] Erin is young.[(triple12)] Harry is green.[(triple13)] Harry is quiet.[(triple14)] Harry is young.[(triple15 OR ((triple13 triple14) -> rule3))] @1: Harry is round.[(((triple15) -> rule2) OR ((((triple13 triple14) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
((triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple7
((triple10) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
((triple12) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
((triple13 triple14) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple15) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple13 triple14) -> (rule3 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2