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