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