Bob is furry. Bob is kind. Bob is red. Bob is young. Erin is furry. Erin is kind. Erin is rough. Fiona is furry. Fiona is kind. Fiona is round. Harry is kind. Harry is young. If someone is rough then they are kind. If someone is red then they are round. Red, furry people are round. Furry people are red. Round, rough people are kind. All kind, young people are furry.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Red, furry people are round.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Round, rough people are kind.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All kind, young people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Bob is red.
True
1
proof
[(triple3 OR ((triple1) -> rule4) OR ((((triple2 triple4) -> rule6)) -> rule4))]
("Bob" "is" "red" "+")
triple3
((triple1) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2 triple4) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is not rough.
False
1
inv-proof
[(triple7)]
("Erin" "is" "rough" "-")
triple7
Erin is red.
True
2
proof
[(((triple5) -> rule4))]
("Erin" "is" "red" "+")
((triple5) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Harry is not furry.
False
3
inv-proof
[(((triple11 triple12) -> rule6))]
("Harry" "is" "furry" "-")
((triple11 triple12) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is round.
True
3
proof
[(((((triple5) -> rule4)) -> rule2) OR ((((triple5) -> rule4) triple5) -> rule3))]
("Erin" "is" "round" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple5) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule2) OR ((((triple5) -> rule4) triple5) -> rule3))]
("Erin" "is" "round" "-")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple5) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Harry is round.
True
5
proof
[(((((((triple11 triple12) -> rule6)) -> rule4)) -> rule2) OR ((((((triple11 triple12) -> rule6)) -> rule4) ((triple11 triple12) -> rule6)) -> rule3))]
("Harry" "is" "round" "+")
((((((triple11 triple12) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple11 triple12) -> (rule6 % int3))) -> (rule4 % int2)) ((triple11 triple12) -> (rule6 % int3))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not round.
False
5
inv-proof
[(((((((triple11 triple12) -> rule6)) -> rule4)) -> rule2) OR ((((((triple11 triple12) -> rule6)) -> rule4) ((triple11 triple12) -> rule6)) -> rule3))]
("Harry" "is" "round" "-")
((((((triple11 triple12) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple11 triple12) -> (rule6 % int3))) -> (rule4 % int2)) ((triple11 triple12) -> (rule6 % int3))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Bob is furry.[(triple1 OR ((triple2 triple4) -> rule6))] Bob is kind.[(triple2)] Bob is red.[(triple3 OR ((triple1) -> rule4) OR ((((triple2 triple4) -> rule6)) -> rule4))] Bob is young.[(triple4)] Erin is furry.[(triple5)] Erin is kind.[(triple6 OR ((triple7) -> rule1) OR ((((((triple5) -> rule4)) -> rule2) triple7) -> rule5) OR ((((((triple5) -> rule4) triple5) -> rule3) triple7) -> rule5))] Erin is rough.[(triple7)] Fiona is furry.[(triple8)] Fiona is kind.[(triple9)] Fiona is round.[(triple10 OR ((((triple8) -> rule4)) -> rule2) OR ((((triple8) -> rule4) triple8) -> rule3))] Harry is kind.[(triple11)] Harry is young.[(triple12)] @1: Bob is round.[(((triple3) -> rule2) OR ((triple3 triple1) -> rule3) OR ((((triple1) -> rule4)) -> rule2) OR ((triple3 ((triple2 triple4) -> rule6)) -> rule3) OR ((((triple1) -> rule4) triple1) -> rule3) OR ((((triple1) -> rule4) ((triple2 triple4) -> rule6)) -> rule3) OR ((((((triple2 triple4) -> rule6)) -> rule4)) -> rule2) OR ((((((triple2 triple4) -> rule6)) -> rule4) triple1) -> rule3) OR ((((((triple2 triple4) -> rule6)) -> rule4) ((triple2 triple4) -> rule6)) -> rule3))] Erin is red.[(((triple5) -> rule4))] Fiona is red.[(((triple8) -> rule4))] Harry is furry.[(((triple11 triple12) -> rule6))] @2: Erin is round.[(((((triple5) -> rule4)) -> rule2) OR ((((triple5) -> rule4) triple5) -> rule3))] Harry is red.[(((((triple11 triple12) -> rule6)) -> rule4))] @3: Harry is round.[(((((((triple11 triple12) -> rule6)) -> rule4)) -> rule2) OR ((((((triple11 triple12) -> rule6)) -> rule4) ((triple11 triple12) -> rule6)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple2 triple4) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
((triple1) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((((triple2 triple4) -> (rule6 % int2))) -> (rule4 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple4
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((triple7) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((((((triple5) -> (rule4 % int3))) -> (rule2 % int2)) triple7) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2)) triple7) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is kind.
("Fiona" "is" "kind" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
((((triple8) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple8) -> (rule4 % int2)) triple8) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Bob is round.
("Bob" "is" "round" "+")
((triple3) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple3 triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((triple3 ((triple2 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple2 triple4) -> (rule6 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((((triple2 triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple2 triple4) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple2 triple4) -> (rule6 % int3))) -> (rule4 % int2)) ((triple2 triple4) -> (rule6 % int3))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((triple5) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple8) -> (rule4 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple11 triple12) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple5) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple11 triple12) -> (rule6 % int2))) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple11 triple12) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple11 triple12) -> (rule6 % int3))) -> (rule4 % int2)) ((triple11 triple12) -> (rule6 % int3))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3