Bob is rough. Bob is not round. Dave is blue. Dave is cold. Dave is round. Erin is blue. Erin is not cold. Erin is green. Erin is kind. Erin is rough. Erin is smart. Fiona is blue. Fiona is rough. Fiona is round. Fiona is smart. Kind people are smart. If someone is green and rough then they are smart. If someone is rough then they are kind. If Bob is blue then Bob is not cold. If Bob is kind then Bob is cold. If someone is cold and blue then they are rough. All cold, blue people are rough. If Bob is not blue then Bob is not rough.
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not round.
("Bob" "is" "round" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is green and rough then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If Bob is blue then Bob is not cold.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "cold" "-"))
If Bob is kind then Bob is cold.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "cold" "+"))
If someone is cold and blue then they are rough.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All cold, blue people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Bob is not blue then Bob is not rough.
((("Bob" "is" "blue" "~")) -> ("Bob" "is" "rough" "-"))
Bob is rough.
True
1
proof
[(triple1)]
("Bob" "is" "rough" "+")
triple1
Fiona is not blue.
False
1
inv-proof
[(triple12)]
("Fiona" "is" "blue" "-")
triple12
Fiona is kind.
True
2
proof
[(((triple13) -> rule3))]
("Fiona" "is" "kind" "+")
((triple13) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Dave is not rough.
False
3
inv-proof
[(((triple4 triple3) -> rule6) OR ((triple4 triple3) -> rule7))]
("Dave" "is" "rough" "-")
((triple4 triple3) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple4 triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Bob is cold.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("Bob" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Bob" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is smart.
True
5
proof
[(((((((triple4 triple3) -> rule6)) -> rule3)) -> rule1) OR ((((((triple4 triple3) -> rule7)) -> rule3)) -> rule1))]
("Dave" "is" "smart" "+")
((((((triple4 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple4 triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((((((triple4 triple3) -> rule6)) -> rule3)) -> rule1) OR ((((((triple4 triple3) -> rule7)) -> rule3)) -> rule1))]
("Dave" "is" "smart" "-")
((((((triple4 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple4 triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is not round.[(triple2)] Bob is rough.[(triple1)] Dave is blue.[(triple3)] Dave is cold.[(triple4)] Dave is round.[(triple5)] Erin is blue.[(triple6)] Erin is green.[(triple8)] Erin is kind.[(triple9 OR ((triple10) -> rule3))] Erin is not cold.[(triple7)] Erin is rough.[(triple10)] Erin is smart.[(triple11 OR ((triple9) -> rule1) OR ((triple8 triple10) -> rule2) OR ((((triple10) -> rule3)) -> rule1))] Fiona is blue.[(triple12)] Fiona is rough.[(triple13)] Fiona is round.[(triple14)] Fiona is smart.[(triple15 OR ((((triple13) -> rule3)) -> rule1))] @1: Bob is kind.[(((triple1) -> rule3))] Dave is rough.[(((triple4 triple3) -> rule6) OR ((triple4 triple3) -> rule7))] Fiona is kind.[(((triple13) -> rule3))] @2: Bob is cold.[(((((triple1) -> rule3)) -> rule5))] Bob is smart.[(((((triple1) -> rule3)) -> rule1))] Dave is kind.[(((((triple4 triple3) -> rule6)) -> rule3) OR ((((triple4 triple3) -> rule7)) -> rule3))] @3: Dave is smart.[(((((((triple4 triple3) -> rule6)) -> rule3)) -> rule1) OR ((((((triple4 triple3) -> rule7)) -> rule3)) -> rule1))]
Bob is not round.
("Bob" "is" "round" "-")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is kind.
("Erin" "is" "kind" "+")
triple9
((triple10) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
((triple9) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple8 triple10) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple12
Fiona is rough.
("Fiona" "is" "rough" "+")
triple13
Fiona is round.
("Fiona" "is" "round" "+")
triple14
Fiona is smart.
("Fiona" "is" "smart" "+")
triple15
((((triple13) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple4 triple3) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((triple4 triple3) -> (rule7 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple13) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple4 triple3) -> (rule6 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((((triple4 triple3) -> (rule7 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple4 triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple4 triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3