Bob is rough. Bob is round. Bob is white. Erin is big. Erin is blue. Erin is kind. Harry is big. Harry is blue. Harry is not kind. Harry is rough. Harry is not round. Harry is smart. If Erin is white and Erin is round then Erin is kind. All blue people are smart. If someone is big and round then they are smart. If someone is kind and round then they are blue. If Erin is smart then Erin is round. If someone is round then they are rough.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If Erin is white and Erin is round then Erin is kind.
((("Erin" "is" "white" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "kind" "+"))
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and round then they are smart.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind and round then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Erin is smart then Erin is round.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "round" "+"))
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Harry is rough.
True
1
proof
[(triple10)]
("Harry" "is" "rough" "+")
triple10
Harry is not big.
False
1
inv-proof
[(triple7)]
("Harry" "is" "big" "-")
triple7
Erin is smart.
True
2
proof
[(((triple5) -> rule2))]
("Erin" "is" "smart" "+")
((triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple5) -> rule2))]
("Erin" "is" "smart" "-")
((triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
True
3
proof
[(((((triple5) -> rule2)) -> rule5))]
("Erin" "is" "round" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not round.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule5))]
("Erin" "is" "round" "-")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
True
4
proof
[(((((((triple5) -> rule2)) -> rule5)) -> rule6))]
("Erin" "is" "rough" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not rough.
False
4
inv-proof
[(((((((triple5) -> rule2)) -> rule5)) -> rule6))]
("Erin" "is" "rough" "-")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Bob" "is" "smart" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is rough.[(triple1 OR ((triple2) -> rule6))] Bob is round.[(triple2)] Bob is white.[(triple3)] Erin is big.[(triple4)] Erin is blue.[(triple5)] Erin is kind.[(triple6)] Harry is big.[(triple7)] Harry is blue.[(triple8)] Harry is not kind.[(triple9)] Harry is not round.[(triple11)] Harry is rough.[(triple10)] Harry is smart.[(triple12 OR ((triple8) -> rule2))] @1: Erin is smart.[(((triple5) -> rule2))] @2: Erin is round.[(((((triple5) -> rule2)) -> rule5))] @3: Erin is rough.[(((((((triple5) -> rule2)) -> rule5)) -> rule6))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
((triple2) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is not kind.
("Harry" "is" "kind" "-")
triple9
Harry is not round.
("Harry" "is" "round" "-")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple8) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3