Bob is cold. Bob is nice. Bob is not red. Bob is smart. Bob is white. Erin is not big. Erin is round. Erin is not white. Fiona is big. Fiona is cold. Fiona is nice. Fiona is red. Fiona is not round. Fiona is smart. Fiona is white. If something is nice and not red then it is smart. Nice things are smart. If something is smart then it is big.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is not white.
("Erin" "is" "white" "-")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is nice and not red then it is smart.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "is" "smart" "+"))
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Bob is smart.
True
1
proof
[(triple4 OR ((triple2) -> rule2) OR ((triple2 triple3) -> rule1))]
("Bob" "is" "smart" "+")
triple4
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple2 triple3) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is big.
False
1
inv-proof
[(triple6)]
("Erin" "is" "big" "+")
triple6
Bob is big.
True
2
proof
[(((triple4) -> rule3) OR ((((triple2) -> rule2)) -> rule3) OR ((((triple2 triple3) -> rule1)) -> rule3))]
("Bob" "is" "big" "+")
((triple4) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not big.
False
2
inv-proof
[(((triple4) -> rule3) OR ((((triple2) -> rule2)) -> rule3) OR ((((triple2 triple3) -> rule1)) -> rule3))]
("Bob" "is" "big" "-")
((triple4) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is nice.[(triple2)] Bob is not red.[(triple3)] Bob is smart.[(triple4 OR ((triple2) -> rule2) OR ((triple2 triple3) -> rule1))] Bob is white.[(triple5)] Erin is not big.[(triple6)] Erin is not white.[(triple8)] Erin is round.[(triple7)] Fiona is big.[(triple9 OR ((triple14) -> rule3) OR ((((triple11) -> rule2)) -> rule3))] Fiona is cold.[(triple10)] Fiona is nice.[(triple11)] Fiona is not round.[(triple13)] Fiona is red.[(triple12)] Fiona is smart.[(triple14 OR ((triple11) -> rule2))] Fiona is white.[(triple15)] @1: Bob is big.[(((triple4) -> rule3) OR ((((triple2) -> rule2)) -> rule3) OR ((((triple2 triple3) -> rule1)) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is not red.
("Bob" "is" "red" "-")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple2 triple3) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple5
Erin is not big.
("Erin" "is" "big" "-")
triple6
Erin is not white.
("Erin" "is" "white" "-")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple9
((triple14) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
Fiona is not round.
("Fiona" "is" "round" "-")
triple13
Fiona is red.
("Fiona" "is" "red" "+")
triple12
Fiona is smart.
("Fiona" "is" "smart" "+")
triple14
((triple11) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple15
Bob is big.
("Bob" "is" "big" "+")
((triple4) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2