Bob is nice. Dave is big. Erin is green. Fiona is red. If Fiona is red then Fiona is big. If something is smart and nice then it is round. Red, smart things are big.
Bob is nice.
("Bob" "is" "nice" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If Fiona is red then Fiona is big.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "big" "+"))
If something is smart and nice then it is round.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Red, smart things are big.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Bob is not nice.
False
1
inv-proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Fiona is big.
True
2
proof
[(((triple4) -> rule1))]
("Fiona" "is" "big" "+")
((triple4) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple4) -> rule1))]
("Fiona" "is" "big" "-")
((triple4) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is nice.[(triple1)] Dave is big.[(triple2)] Erin is green.[(triple3)] Fiona is red.[(triple4)] @1: Fiona is big.[(((triple4) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
((triple4) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1