Dave is green. Fiona is big. If someone is big then they are furry. All quiet people are rough. Green people are not rough. Young people are rough. If someone is furry then they are green. If Dave is young and Dave is cold then Dave is not quiet. If someone is cold and quiet then they are young. If Fiona is not big and Fiona is not young then Fiona is rough.
Dave is green.
("Dave" "is" "green" "+")
Fiona is big.
("Fiona" "is" "big" "+")
If someone is big then they are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Green people are not rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "-"))
Young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If Dave is young and Dave is cold then Dave is not quiet.
((("Dave" "is" "young" "+") ("Dave" "is" "cold" "+")) -> ("Dave" "is" "quiet" "-"))
If someone is cold and quiet then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Fiona is not big and Fiona is not young then Fiona is rough.
((("Fiona" "is" "big" "~") ("Fiona" "is" "young" "~")) -> ("Fiona" "is" "rough" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Fiona is not big.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "big" "-")
triple2
Dave is not rough.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Fiona is not furry.
False
2
inv-proof
[(((triple2) -> rule1))]
("Fiona" "is" "furry" "-")
((triple2) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Fiona" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is not green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Fiona" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is not rough.
True
4
proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
("Fiona" "is" "rough" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is rough.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
("Fiona" "is" "rough" "+")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "young" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "young" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Dave is green.[(triple1)] Fiona is big.[(triple2)] @1: Dave is not rough.[(((triple1) -> rule3))] Fiona is furry.[(((triple2) -> rule1))] @2: Fiona is green.[(((((triple2) -> rule1)) -> rule5))] @3: Fiona is not rough.[(((((((triple2) -> rule1)) -> rule5)) -> rule3))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Dave is not rough.
("Dave" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple2) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is not rough.
("Fiona" "is" "rough" "-")
((((((triple2) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3