Bob is rough. Erin is big. Harry is big. Harry is furry. Harry is rough. Harry is round. Harry is smart. All rough people are red. If Erin is big then Erin is round. Round people are rough.
Bob is rough.
("Bob" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Erin is big then Erin is round.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "round" "+"))
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Harry is furry.
True
1
proof
[(triple4)]
("Harry" "is" "furry" "+")
triple4
Harry is not smart.
False
1
inv-proof
[(triple7)]
("Harry" "is" "smart" "-")
triple7
Harry is red.
True
2
proof
[(((triple5) -> rule1) OR ((((triple6) -> rule3)) -> rule1))]
("Harry" "is" "red" "+")
((triple5) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule2))]
("Erin" "is" "round" "-")
((triple2) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Erin" "is" "rough" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Erin" "is" "rough" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
True
4
proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Erin" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not red.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Erin" "is" "red" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is rough.[(triple1)] Erin is big.[(triple2)] Harry is big.[(triple3)] Harry is furry.[(triple4)] Harry is rough.[(triple5 OR ((triple6) -> rule3))] Harry is round.[(triple6)] Harry is smart.[(triple7)] @1: Bob is red.[(((triple1) -> rule1))] Erin is round.[(((triple2) -> rule2))] Harry is red.[(((triple5) -> rule1) OR ((((triple6) -> rule3)) -> rule1))] @2: Erin is rough.[(((((triple2) -> rule2)) -> rule3))] @3: Erin is red.[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
triple5
((triple6) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple5) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3