Bob is big. Dave is cold. Erin is big. If something is smart then it is rough. All young things are big. All cold, smart things are rough. If Erin is big then Erin is smart. All big, smart things are cold. If Dave is blue then Dave is cold.
Bob is big.
("Bob" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is big.
("Erin" "is" "big" "+")
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All cold, smart things are rough.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Erin is big then Erin is smart.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "smart" "+"))
All big, smart things are cold.
((("something" "is" "big" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Dave is blue then Dave is cold.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "cold" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple2)]
("Dave" "is" "cold" "-")
triple2
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is big.[(triple1)] Dave is cold.[(triple2)] Erin is big.[(triple3)] @1: Erin is smart.[(((triple3) -> rule4))] @2: Erin is cold.[(((triple3 ((triple3) -> rule4)) -> rule5))] Erin is rough.[(((((triple3) -> rule4)) -> rule1) OR ((((triple3 ((triple3) -> rule4)) -> rule5) ((triple3) -> rule4)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule5 % int2)) ((triple3) -> (rule4 % int3))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3