Bob is big. Bob is quiet. Dave is cold. Dave is kind. Fiona is cold. Fiona is green. Gary is green. All cold people are kind. If someone is quiet and cold then they are green. All big, smart people are young. Kind, quiet people are smart. If someone is big and young then they are green. Kind, green people are quiet. All smart people are green. If someone is green and smart then they are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is green.
("Gary" "is" "green" "+")
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and cold then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All big, smart people are young.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Kind, quiet people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and young then they are green.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Kind, green people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is green and smart then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
Dave is kind.
True
1
proof
[(triple4 OR ((triple3) -> rule1))]
("Dave" "is" "kind" "+")
triple4
((triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is not green.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "green" "-")
triple6
Fiona is kind.
True
2
proof
[(((triple5) -> rule1))]
("Fiona" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple5) -> rule1))]
("Fiona" "is" "kind" "-")
((triple5) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
True
4
proof
[(((((triple5) -> rule1) triple6) -> rule6))]
("Fiona" "is" "quiet" "+")
((((triple5) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not quiet.
False
4
inv-proof
[(((((triple5) -> rule1) triple6) -> rule6))]
("Fiona" "is" "quiet" "-")
((((triple5) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@5: Bob is green.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule4 <- rule1 <- rule8 <- FAIL)]]
("Bob" "is" "green" "-")
Gary is quiet.
Unknown
rconc
[@4: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule8 <- rule4 <- FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not cold.
Unknown
inv-rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule1 <- FAIL)]]
("Gary" "is" "cold" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is quiet.[(triple2)] Dave is cold.[(triple3)] Dave is kind.[(triple4 OR ((triple3) -> rule1))] Fiona is cold.[(triple5)] Fiona is green.[(triple6)] Gary is green.[(triple7)] @1: Fiona is kind.[(((triple5) -> rule1))] @2: Fiona is quiet.[(((((triple5) -> rule1) triple6) -> rule6))] @3: Fiona is smart.[(((((triple5) -> rule1) ((((triple5) -> rule1) triple6) -> rule6)) -> rule4))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
((triple3) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple5) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple5) -> (rule1 % int3)) ((((triple5) -> (rule1 % int3)) triple6) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3