Bob is big. Bob is blue. Bob is nice. Bob is rough. Erin is big. Erin is blue. Erin is furry. Erin is kind. Erin is nice. Erin is rough. Fiona is big. Fiona is blue. Harry is big. Harry is blue. Harry is rough. Harry is smart. If Fiona is nice then Fiona is big. Blue things are rough. Rough, smart things are nice. If something is furry then it is rough. All smart, nice things are big. All smart things are furry. If something is big and rough then it is nice. If something is blue and nice then it is furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Fiona is nice then Fiona is big.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "big" "+"))
Blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Rough, smart things are nice.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All smart, nice things are big.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is big and rough then it is nice.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is blue and nice then it is furry.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Harry is rough.
True
1
proof
[(triple15 OR ((triple14) -> rule2) OR ((((triple16) -> rule6)) -> rule4))]
("Harry" "is" "rough" "+")
triple15
((triple14) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple16) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Erin is not rough.
False
1
inv-proof
[(triple10 OR ((triple6) -> rule2) OR ((triple7) -> rule4) OR ((((triple6 triple9) -> rule8)) -> rule4))]
("Erin" "is" "rough" "-")
triple10
((triple6) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple7) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6 triple9) -> (rule8 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Fiona is rough.
True
2
proof
[(((triple12) -> rule2))]
("Fiona" "is" "rough" "+")
((triple12) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple12) -> rule2))]
("Fiona" "is" "rough" "-")
((triple12) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is nice.
True
4
proof
[(((triple11 ((triple12) -> rule2)) -> rule7))]
("Fiona" "is" "nice" "+")
((triple11 ((triple12) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not nice.
False
4
inv-proof
[(((triple11 ((triple12) -> rule2)) -> rule7))]
("Fiona" "is" "nice" "-")
((triple11 ((triple12) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
True
6
proof
[(((triple12 ((triple11 ((triple12) -> rule2)) -> rule7)) -> rule8))]
("Fiona" "is" "furry" "+")
((triple12 ((triple11 ((triple12) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not furry.
False
6
inv-proof
[(((triple12 ((triple11 ((triple12) -> rule2)) -> rule7)) -> rule8))]
("Fiona" "is" "furry" "-")
((triple12 ((triple11 ((triple12) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is nice.[(triple3 OR ((triple1 triple4) -> rule7) OR ((triple1 ((triple2) -> rule2)) -> rule7))] Bob is rough.[(triple4 OR ((triple2) -> rule2) OR ((((triple2 triple3) -> rule8)) -> rule4))] Erin is big.[(triple5)] Erin is blue.[(triple6)] Erin is furry.[(triple7 OR ((triple6 triple9) -> rule8) OR ((triple6 ((triple5 triple10) -> rule7)) -> rule8) OR ((triple6 ((triple5 ((triple6) -> rule2)) -> rule7)) -> rule8))] Erin is kind.[(triple8)] Erin is nice.[(triple9 OR ((triple5 triple10) -> rule7) OR ((triple5 ((triple6) -> rule2)) -> rule7) OR ((triple5 ((triple7) -> rule4)) -> rule7))] Erin is rough.[(triple10 OR ((triple6) -> rule2) OR ((triple7) -> rule4) OR ((((triple6 triple9) -> rule8)) -> rule4))] Fiona is big.[(triple11)] Fiona is blue.[(triple12)] Harry is big.[(triple13 OR ((triple16 ((triple15 triple16) -> rule3)) -> rule5) OR ((triple16 ((((triple14) -> rule2) triple16) -> rule3)) -> rule5) OR ((triple16 ((((((triple16) -> rule6)) -> rule4) triple16) -> rule3)) -> rule5))] Harry is blue.[(triple14)] Harry is rough.[(triple15 OR ((triple14) -> rule2) OR ((((triple16) -> rule6)) -> rule4))] Harry is smart.[(triple16)] @1: Bob is furry.[(((triple2 triple3) -> rule8) OR ((triple2 ((triple1 triple4) -> rule7)) -> rule8) OR ((triple2 ((triple1 ((triple2) -> rule2)) -> rule7)) -> rule8))] Fiona is rough.[(((triple12) -> rule2))] Harry is furry.[(((triple16) -> rule6) OR ((triple14 ((triple13 triple15) -> rule7)) -> rule8) OR ((triple14 ((triple15 triple16) -> rule3)) -> rule8) OR ((triple14 ((triple13 ((triple14) -> rule2)) -> rule7)) -> rule8) OR ((triple14 ((((triple14) -> rule2) triple16) -> rule3)) -> rule8))] Harry is nice.[(((triple13 triple15) -> rule7) OR ((triple15 triple16) -> rule3) OR ((triple13 ((triple14) -> rule2)) -> rule7) OR ((((triple14) -> rule2) triple16) -> rule3) OR ((triple13 ((((triple16) -> rule6)) -> rule4)) -> rule7) OR ((((((triple16) -> rule6)) -> rule4) triple16) -> rule3))] @2: Fiona is nice.[(((triple11 ((triple12) -> rule2)) -> rule7))] @3: Fiona is furry.[(((triple12 ((triple11 ((triple12) -> rule2)) -> rule7)) -> rule8))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1 triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple1 ((triple2) -> (rule2 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple2) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2 triple3) -> (rule8 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
((triple6 triple9) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple6 ((triple5 triple10) -> (rule7 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple6 ((triple5 ((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
((triple5 triple10) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple5 ((triple6) -> (rule2 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((triple5 ((triple7) -> (rule4 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple10
((triple6) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple7) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6 triple9) -> (rule8 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple11
Fiona is blue.
("Fiona" "is" "blue" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
((triple16 ((triple15 triple16) -> (rule3 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple16 ((((triple14) -> (rule2 % int3)) triple16) -> (rule3 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((triple16 ((((((triple16) -> (rule6 % int4))) -> (rule4 % int3)) triple16) -> (rule3 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
((triple14) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple16) -> (rule6 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Bob is furry.
("Bob" "is" "furry" "+")
((triple2 triple3) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple2 ((triple1 triple4) -> (rule7 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple2 ((triple1 ((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple12) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple16) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple14 ((triple13 triple15) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple14 ((triple15 triple16) -> (rule3 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple14 ((triple13 ((triple14) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((triple14 ((((triple14) -> (rule2 % int3)) triple16) -> (rule3 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple13 triple15) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple15 triple16) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple13 ((triple14) -> (rule2 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple14) -> (rule2 % int2)) triple16) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple13 ((((triple16) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple16) -> (rule6 % int3))) -> (rule4 % int2)) triple16) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple11 ((triple12) -> (rule2 % int2))) -> (rule7 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple12 ((triple11 ((triple12) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3