Bob is big. Bob is cold. Bob is furry. Bob is nice. Bob is rough. Bob is white. Bob is young. Gary is rough. Harry is big. Harry is nice. Harry is white. Harry is young. If someone is rough then they are big. All big people are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is rough then they are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Bob is young.
True
1
proof
[(triple7 OR ((triple1) -> rule2) OR ((((triple5) -> rule1)) -> rule2))]
("Bob" "is" "young" "+")
triple7
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Harry is not white.
False
1
inv-proof
[(triple11)]
("Harry" "is" "white" "-")
triple11
Gary is big.
True
2
proof
[(((triple8) -> rule1))]
("Gary" "is" "big" "+")
((triple8) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple8) -> rule1))]
("Gary" "is" "big" "-")
((triple8) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
True
3
proof
[(((((triple8) -> rule1)) -> rule2))]
("Gary" "is" "young" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule2))]
("Gary" "is" "young" "-")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Bob is big.[(triple1 OR ((triple5) -> rule1))] Bob is cold.[(triple2)] Bob is furry.[(triple3)] Bob is nice.[(triple4)] Bob is rough.[(triple5)] Bob is white.[(triple6)] Bob is young.[(triple7 OR ((triple1) -> rule2) OR ((((triple5) -> rule1)) -> rule2))] Gary is rough.[(triple8)] Harry is big.[(triple9)] Harry is nice.[(triple10)] Harry is white.[(triple11)] Harry is young.[(triple12 OR ((triple9) -> rule2))] @1: Gary is big.[(((triple8) -> rule1))] @2: Gary is young.[(((((triple8) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((triple5) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple1) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
((triple9) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple8) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2